let x be ExtReal; :: according to XXREAL_2:def 12 :: thesis: for s being ExtReal st x in [.r,s.] & s in [.r,s.] holds

[.x,s.] c= [.r,s.]

let y be ExtReal; :: thesis: ( x in [.r,s.] & y in [.r,s.] implies [.x,y.] c= [.r,s.] )

assume x in [.r,s.] ; :: thesis: ( not y in [.r,s.] or [.x,y.] c= [.r,s.] )

then A1: r <= x by XXREAL_1:1;

assume y in [.r,s.] ; :: thesis: [.x,y.] c= [.r,s.]

then A2: y <= s by XXREAL_1:1;

let z be ExtReal; :: according to MEMBERED:def 8 :: thesis: ( not z in [.x,y.] or z in [.r,s.] )

assume A3: z in [.x,y.] ; :: thesis: z in [.r,s.]

then x <= z by XXREAL_1:1;

then A4: r <= z by A1, XXREAL_0:2;

z <= y by A3, XXREAL_1:1;

then z <= s by A2, XXREAL_0:2;

hence z in [.r,s.] by A4, XXREAL_1:1; :: thesis: verum

[.x,s.] c= [.r,s.]

let y be ExtReal; :: thesis: ( x in [.r,s.] & y in [.r,s.] implies [.x,y.] c= [.r,s.] )

assume x in [.r,s.] ; :: thesis: ( not y in [.r,s.] or [.x,y.] c= [.r,s.] )

then A1: r <= x by XXREAL_1:1;

assume y in [.r,s.] ; :: thesis: [.x,y.] c= [.r,s.]

then A2: y <= s by XXREAL_1:1;

let z be ExtReal; :: according to MEMBERED:def 8 :: thesis: ( not z in [.x,y.] or z in [.r,s.] )

assume A3: z in [.x,y.] ; :: thesis: z in [.r,s.]

then x <= z by XXREAL_1:1;

then A4: r <= z by A1, XXREAL_0:2;

z <= y by A3, XXREAL_1:1;

then z <= s by A2, XXREAL_0:2;

hence z in [.r,s.] by A4, XXREAL_1:1; :: thesis: verum