let r, s be ExtReal; :: according to XXREAL_2:def 12 :: thesis: ( r in A /\ B & s in A /\ B implies [.r,s.] c= A /\ B )

assume that

A1: r in A /\ B and

A2: s in A /\ B ; :: thesis: [.r,s.] c= A /\ B

A3: s in B by A2, XBOOLE_0:def 4;

r in B by A1, XBOOLE_0:def 4;

then A4: [.r,s.] c= B by A3, Def12;

A5: s in A by A2, XBOOLE_0:def 4;

r in A by A1, XBOOLE_0:def 4;

then [.r,s.] c= A by A5, Def12;

hence [.r,s.] c= A /\ B by A4, XBOOLE_1:19; :: thesis: verum

assume that

A1: r in A /\ B and

A2: s in A /\ B ; :: thesis: [.r,s.] c= A /\ B

A3: s in B by A2, XBOOLE_0:def 4;

r in B by A1, XBOOLE_0:def 4;

then A4: [.r,s.] c= B by A3, Def12;

A5: s in A by A2, XBOOLE_0:def 4;

r in A by A1, XBOOLE_0:def 4;

then [.r,s.] c= A by A5, Def12;

hence [.r,s.] c= A /\ B by A4, XBOOLE_1:19; :: thesis: verum