let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the_set_of_all_open_real_bounded_intervals or x in { I where I is Subset of REAL : I is open_interval } )
assume x in the_set_of_all_open_real_bounded_intervals ; :: thesis: x in { I where I is Subset of REAL : I is open_interval }
then consider a, b being Real such that
A2: x = ].a,b.[ ;
reconsider x1 = x as Subset of REAL by A2;
( a is Element of ExtREAL & b is Element of ExtREAL ) by NUMBERS:31, XREAL_0:def 1;
then x1 is open_interval by A2, MEASURE5:def 2;
hence x in { I where I is Subset of REAL : I is open_interval } ; :: thesis: verum