let I be set ; :: thesis: for C being Subset of I holds C * c= I *
let C be Subset of I; :: thesis: C * c= I *
thus C * c= I * :: thesis: verum

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in C * or a in I * )
assume a in C * ; :: thesis: a in I *
then reconsider p = a as FinSequence of C by FINSEQ_1:def 11;
rng p c= I by XBOOLE_1:1;
then p is FinSequence of I by FINSEQ_1:def 4;
hence a in I * by FINSEQ_1:def 11; :: thesis: verum

end;