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 |.r.| <= 1 & x in M /\ N holds
r * x in M /\ N
let r be Real; :: thesis: ( |.r.| <= 1 & x in M /\ N implies r * x in M /\ N )
assume that
A1: |.r.| <= 1 and
A2: x in M /\ N ; :: thesis: r * x in M /\ N
x in N by A2, XBOOLE_0:def 4;
then A3: r * x in N by A1, Def1;
x in M by A2, XBOOLE_0:def 4;
then r * x in M by A1, Def1;
hence r * x in M /\ N by A3, XBOOLE_0:def 4; :: thesis: verum