set S1 = {{}} \/ { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } ;
set S2 = { s where s is Subset of REAL : ex a, b being Real st
( a <= b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } ;
A1: {{}} \/ { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } c= { s where s is Subset of REAL : ex a, b being Real st
( a <= b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {{}} \/ { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } or x in { s where s is Subset of REAL : ex a, b being Real st
( a <= b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } )
assume x in {{}} \/ { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } ; :: thesis: x in { s where s is Subset of REAL : ex a, b being Real st
( a <= b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) }
then A2: ( x in {{}} or x in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } ) by XBOOLE_0:def 3;
A3: ( x = {} implies x in { s where s is Subset of REAL : ex a, b being Real st
( a <= b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } )

proof

set a = 0 ;
set b = 0 ;
set s0 = ].0,0.];
for x being real number holds
( x in ].0,0.] iff ( 0 < x & x <= 0 ) ) ;
hence ( x = {} implies x in { s where s is Subset of REAL : ex a, b being Real st
( a <= b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } ) ; :: thesis: verum

end;

( x in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } implies x in { s where s is Subset of REAL : ex a, b being Real st
( a <= b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } )

proof

assume x in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for t being real number holds
( t in s iff ( a < t & t <= b ) ) ) ) } ; :: thesis: x in { s where s is Subset of REAL : ex a, b being Real st
( a <= b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) }
then consider s0 being Subset of REAL such that
A4: ( s0 = x & ex a, b being Real st
( a < b & ( for t being real number holds
( t in s0 iff ( a < t & t <= b ) ) ) ) ) ;
thus x in { s where s is Subset of REAL : ex a, b being Real st
( a <= b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } by A4; :: thesis: verum

end;

hence x in { s where s is Subset of REAL : ex a, b being Real st
( a <= b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } by A2, A3, TARSKI:def 1; :: thesis: verum

end;

{ s where s is Subset of REAL : ex a, b being Real st
( a <= b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } c= {{}} \/ { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { s where s is Subset of REAL : ex a, b being Real st
( a <= b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } or x in {{}} \/ { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } )
assume x in { s where s is Subset of REAL : ex a, b being Real st
( a <= b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } ; :: thesis: x in {{}} \/ { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) }
then consider s0 being Subset of REAL such that
A5: x = s0 and
A6: ex a, b being Real st
( a <= b & ( for t being real number holds
( t in s0 iff ( a < t & t <= b ) ) ) ) ;
consider a, b being Real such that
A7: a <= b and
A8: for t being real number holds
( t in s0 iff ( a < t & t <= b ) ) by A6;
A9: ( a = b implies x in {{}} )

proof

assume a = b ; :: thesis: x in {{}}
then s0 c= {} by A8;
then x = {} by A5;
hence x in {{}} by TARSKI:def 1; :: thesis: verum

end;

( a < b implies x in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } ) by A5, A8;
hence x in {{}} \/ { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } by XBOOLE_0:def 3, XXREAL_0:1, A7, A9; :: thesis: verum

end;

hence {{}} \/ { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } = { s where s is Subset of REAL : ex a, b being Real st
( a <= b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } by A1; :: thesis: verum