let X be set ; :: thesis: ( (X -freeCountableSet) /\ X = {} & X -freeCountableSet is infinite )
set X2 = proj2 X;
set Y = (bool (proj2 X)) \ (proj2 X);
set y = the Element of (bool (proj2 X)) \ (proj2 X);
set IT = X -freeCountableSet ;
not the Element of (bool (proj2 X)) \ (proj2 X) in proj2 X by XBOOLE_0:def 5;
hence (X -freeCountableSet) /\ X = {} by XBOOLE_0:def 7, Th58; :: thesis: X -freeCountableSet is infinite
thus X -freeCountableSet is infinite ; :: thesis: verum