A1: the_set_of_all_closed_real_bounded_intervals c= { I where I is Subset of REAL : I is closed_interval }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the_set_of_all_closed_real_bounded_intervals or x in { I where I is Subset of REAL : I is closed_interval } )
assume x in the_set_of_all_closed_real_bounded_intervals ; :: thesis: x in { I where I is Subset of REAL : I is closed_interval }
then consider a, b being Real such that
A2: x = [.a,b.] ;
reconsider x1 = x as Subset of REAL by A2;
x1 is closed_interval by A2, MEASURE5:def 3;
hence x in { I where I is Subset of REAL : I is closed_interval } ; :: thesis: verum

end;

{ I where I is Subset of REAL : I is closed_interval } c= the_set_of_all_closed_real_bounded_intervals

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { I where I is Subset of REAL : I is closed_interval } or x in the_set_of_all_closed_real_bounded_intervals )
assume x in { I where I is Subset of REAL : I is closed_interval } ; :: thesis: x in the_set_of_all_closed_real_bounded_intervals
then consider I0 being Subset of REAL such that
A3: x = I0 and
A4: I0 is closed_interval ;
consider a, b being Real such that
A5: I0 = [.a,b.] by A4, MEASURE5:def 3;
thus x in the_set_of_all_closed_real_bounded_intervals by A3, A5; :: thesis: verum

end;

hence the_set_of_all_closed_real_bounded_intervals = { I where I is Subset of REAL : I is closed_interval } by A1; :: thesis: verum