let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the_set_of_all_left_open_real_bounded_intervals or x in { I where I is Subset of REAL : I is left_open_interval } )
assume x in the_set_of_all_left_open_real_bounded_intervals ; :: thesis: x in { I where I is Subset of REAL : I is left_open_interval }
then consider a, b being Real such that
A1: x = ].a,b.] ;
reconsider x1 = x as Subset of REAL by A1;
reconsider a = a as R_eal by XREAL_0:def 1, NUMBERS:31;
x1 = ].a,b.] by A1;
then x1 is left_open_interval by MEASURE5:def 5;
hence x in { I where I is Subset of REAL : I is left_open_interval } ; :: thesis: verum