let V be non empty RLSStruct ; :: thesis: for M, N being Subset of V st M is cone & N is cone holds
M /\ N is cone
let M, N be Subset of V; :: thesis: ( M is cone & N is cone implies M /\ N is cone )
assume that
A1: M is cone and
A2: N is cone ; :: thesis: M /\ N is cone
let r be Real; :: according to CONVEX3:def 3 :: thesis: for v being VECTOR of V st r > 0 & v in M /\ N holds
r * v in M /\ N
let v be VECTOR of V; :: thesis: ( r > 0 & v in M /\ N implies r * v in M /\ N )
assume that
A3: r > 0 and
A4: v in M /\ N ; :: thesis: r * v in M /\ N
v in N by A4, XBOOLE_0:def 4;
then A5: r * v in N by A2, A3;
v in M by A4, XBOOLE_0:def 4;
then r * v in M by A1, A3;
hence r * v in M /\ N by A5, XBOOLE_0:def 4; :: thesis: verum