thus union {NAT} c= FinSETS by CLASSES4:17; :: thesis: ( not union {NAT} in FinSETS & not {NAT} c= FinSETS & not {NAT} in FinSETS )
thus not union {NAT} in FinSETS ; :: thesis: ( not {NAT} c= FinSETS & not {NAT} in FinSETS )
thus not {NAT} c= FinSETS :: thesis: not {NAT} in FinSETS

proof

assume A1: {NAT} c= FinSETS ; :: thesis: contradiction
NAT in {NAT} by TARSKI:def 1;
hence contradiction by A1; :: thesis: verum

end;

assume A2: {NAT} in FinSETS ; :: thesis: contradiction
NAT in {NAT} by TARSKI:def 1;
then NAT in union FinSETS by A2, TARSKI:def 4;
then NAT in FinSETS by CLASSES4:81;
hence contradiction ; :: thesis: verum