let X be set ; :: thesis: ( (X -freeCountableSet) /\ X = {} & not X -freeCountableSet is finite )
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;
then X -freeCountableSet misses X by Th58;
hence (X -freeCountableSet) /\ X = {} by XBOOLE_0:def 7; :: thesis: not X -freeCountableSet is finite
thus not X -freeCountableSet is finite ; :: thesis: verum