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 M or x in N ) by A2, XBOOLE_0:def 3;
then ( r * x in M or r * x in N ) by A1, Def1;
hence r * x in M \/ N by XBOOLE_0:def 3; :: thesis: verum