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