let x be ext-real number ; :: according to XXREAL_2:def 12 :: thesis: for s being ext-real number st x in [.r,s.[ & s in [.r,s.[ holds
[.x,s.] c= [.r,s.[
let y be ext-real number ; :: 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 A10: r <= x by XXREAL_1:3;
assume y in [.r,s.[ ; :: thesis: [.x,y.] c= [.r,s.[
then A11: y < s by XXREAL_1:3;
let z be ext-real number ; :: according to MEMBERED:def 8 :: thesis: ( not z in [.x,y.] or z in [.r,s.[ )
assume A12: z in [.x,y.] ; :: thesis: z in [.r,s.[
then x <= z by XXREAL_1:1;
then A13: r <= z by A10, XXREAL_0:2;
z <= y by A12, XXREAL_1:1;
then z < s by A11, XXREAL_0:2;
hence z in [.r,s.[ by A13, XXREAL_1:3; :: thesis: verum