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