thus
not ].r,s.[ is left_end
:: thesis: not ].r,s.[ is right_end

then A7: sup ].r,s.[ in ].r,s.[ ;

then A8: sup ].r,s.[ < s by XXREAL_1:4;

r < sup ].r,s.[ by A7, XXREAL_1:4;

then r < s by A8, XXREAL_0:2;

then s = sup ].r,s.[ by Th32;

hence contradiction by A7, XXREAL_1:4; :: thesis: verum

proof

assume
].r,s.[ is right_end
; :: thesis: contradiction
assume
].r,s.[ is left_end
; :: thesis: contradiction

then A5: inf ].r,s.[ in ].r,s.[ ;

then A6: inf ].r,s.[ < s by XXREAL_1:4;

r < inf ].r,s.[ by A5, XXREAL_1:4;

then r < s by A6, XXREAL_0:2;

then r = inf ].r,s.[ by Th28;

hence contradiction by A5, XXREAL_1:4; :: thesis: verum

end;then A5: inf ].r,s.[ in ].r,s.[ ;

then A6: inf ].r,s.[ < s by XXREAL_1:4;

r < inf ].r,s.[ by A5, XXREAL_1:4;

then r < s by A6, XXREAL_0:2;

then r = inf ].r,s.[ by Th28;

hence contradiction by A5, XXREAL_1:4; :: thesis: verum

then A7: sup ].r,s.[ in ].r,s.[ ;

then A8: sup ].r,s.[ < s by XXREAL_1:4;

r < sup ].r,s.[ by A7, XXREAL_1:4;

then r < s by A8, XXREAL_0:2;

then s = sup ].r,s.[ by Th32;

hence contradiction by A7, XXREAL_1:4; :: thesis: verum