Fin a c= C

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Fin a or x in C )
assume x in Fin a ; :: thesis: x in C
then x c= a by FINSUB_1:def 5;
hence x in C by CLASSES1:def 1; :: thesis: verum

end;

hence Fin a is non empty preBoolean Subset of C ; :: thesis: verum