let V be RealLinearSpace; :: thesis: for M being Subset of V holds M c= Cir M
let M be Subset of V; :: thesis: M c= Cir M
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in M or u in Cir M )
assume A1: u in M ; :: thesis: u in Cir M
for Y being set st Y in Circled-Family M holds
u in Y

proof

let Y be set ; :: thesis: ( Y in Circled-Family M implies u in Y )
assume A2: Y in Circled-Family M ; :: thesis: u in Y
then reconsider Y = Y as Subset of V ;
M c= Y by A2, Def2;
hence u in Y by A1; :: thesis: verum

end;

hence u in Cir M by SETFAM_1:def 1; :: thesis: verum