the_set_of_all_left_open_real_bounded_intervals = { ].a,b.] where a, b is Real : a <= b }

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { ].a,b.] where a, b is Real : a <= b } c= the_set_of_all_left_open_real_bounded_intervals

let x be object ; :: thesis: ( x in the_set_of_all_left_open_real_bounded_intervals implies b₁ in { ].b,b₃.] where a, b is Real : b <= b₃ } )
assume x in the_set_of_all_left_open_real_bounded_intervals ; :: thesis: b₁ in { ].b,b₃.] where a, b is Real : b <= b₃ }
then consider a, b being Real such that
A1: x = ].a,b.] ;

per cases ( a <= b or not a <= b ) ;

suppose a <= b ; :: thesis: b₁ in { ].b,b₃.] where a, b is Real : b <= b₃ }

hence x in { ].a,b.] where a, b is Real : a <= b } by A1; :: thesis: verum

end;

suppose not a <= b ; :: thesis: b₁ in { ].b,b₃.] where a, b is Real : b <= b₃ }

then x = ].0,0.] by A1, XXREAL_1:26;
hence x in { ].a,b.] where a, b is Real : a <= b } ; :: thesis: verum

end;

end;

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ].a,b.] where a, b is Real : a <= b } or x in the_set_of_all_left_open_real_bounded_intervals )
assume x in { ].a,b.] where a, b is Real : a <= b } ; :: thesis: x in the_set_of_all_left_open_real_bounded_intervals
then ex a, b being Real st
( x = ].a,b.] & a <= b ) ;
hence x in the_set_of_all_left_open_real_bounded_intervals ; :: thesis: verum

end;

hence ( the_set_of_all_left_open_real_bounded_intervals is cap-closed & the_set_of_all_left_open_real_bounded_intervals is diff-finite-partition-closed & the_set_of_all_left_open_real_bounded_intervals is with_empty_element & the_set_of_all_left_open_real_bounded_intervals is with_countable_Cover ) by SRINGS_2:9; :: thesis: verum