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 ) ) ) ) } ;
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= II

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y 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 y in II )
assume y 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: y in II
then consider s0 being Subset of REAL such that
A2: ( y = s0 & ex a, b being Real st
( a <= b & ( for x being real number holds
( x in s0 iff ( a < x & x <= b ) ) ) ) ) ;
consider a0, b0 being Real such that
A3: ( a0 <= b0 & ( for x being real number holds
( x in s0 iff ( a0 < x & x <= b0 ) ) ) ) by A2;
A4: s0 c= ].a0,b0.]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in s0 or x in ].a0,b0.] )
assume A5: x in s0 ; :: thesis: x in ].a0,b0.]
then reconsider x = x as real number ;
( a0 < x & x <= b0 ) by A3, A5;
hence x in ].a0,b0.] ; :: thesis: verum

end;

].a0,b0.] c= s0

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ].a0,b0.] or x in s0 )
assume A6: x in ].a0,b0.] ; :: thesis: x in s0
then reconsider x = x as real number ;
( a0 < x & x <= b0 ) by A6, XXREAL_1:2;
hence x in s0 by A3; :: thesis: verum

end;

then s0 = ].a0,b0.] by A4;
hence y in II by A2, A3; :: thesis: verum

end;

II 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 y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in II or y 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 y in II ; :: thesis: y 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 a0, b0 being Real such that
A7: ( y = ].a0,b0.] & a0 <= b0 ) ;
reconsider y = y as set by TARSKI:1;
for x being real number holds
( x in y iff ( a0 < x & x <= b0 ) ) by A7, XXREAL_1:2;
hence y 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 A7; :: 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 ) ) ) ) } = II by A1; :: thesis: verum