let V be RealLinearSpace; :: thesis: for M, N being circled Subset of V holds M /\ N is circled
let M, N be circled Subset of V; :: thesis: M /\ N is circled
let x be VECTOR of V; :: according to CIRCLED1:def 1 :: thesis: for r being Real st abs r <= 1 & x in M /\ N holds
r * x in M /\ N
let r be Real; :: thesis: ( abs r <= 1 & x in M /\ N implies r * x in M /\ N )
assume A1: ( abs r <= 1 & x in M /\ N ) ; :: thesis: r * x in M /\ N
then ( x in M & x in N ) by XBOOLE_0:def 4;
then ( r * x in M & r * x in N ) by A1, Def1;
hence r * x in M /\ N by XBOOLE_0:def 4; :: thesis: verum