set c = the Element of C;
{} c= the Element of C ;
then {} in C by CLASSES1:def 1;
hence not Sub_of_Fin C is empty by Def3; :: thesis: Sub_of_Fin C is subset-closed
let a, b be set ; :: according to CLASSES1:def 1 :: thesis: ( not a in Sub_of_Fin C or not b c= a or b in Sub_of_Fin C )
assume A1: a in Sub_of_Fin C ; :: thesis: ( not b c= a or b in Sub_of_Fin C )
then A2: a is finite by Def3;
assume A3: b c= a ; :: thesis: b in Sub_of_Fin C
then b in C by A1, CLASSES1:def 1;
hence b in Sub_of_Fin C by A2, A3, Def3; :: thesis: verum