let V be RealLinearSpace; :: thesis: for M1, M2 being Subset of V st M1 c= M2 holds
Cir M1 c= Cir M2
let M1, M2 be Subset of V; :: thesis: ( M1 c= M2 implies Cir M1 c= Cir M2 )
assume A1: M1 c= M2 ; :: thesis: Cir M1 c= Cir M2
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Cir M1 or x in Cir M2 )
assume A2: x in Cir M1 ; :: thesis: x in Cir M2
Circled-Family M2 c= Circled-Family M1 by A1, Th9;
then meet (Circled-Family M1) c= meet (Circled-Family M2) by SETFAM_1:7;
hence x in Cir M2 by A2; :: thesis: verum