Fin a c= C

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Fin a or x in C )
reconsider xx = x as set by TARSKI:1;
assume x in Fin a ; :: thesis: x in C
then xx 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