let I1, I2 be Subset of (REAL n); :: thesis: ( ( for x being object holds
( x in I1 iff ex y being Element of REAL n st
( x = y & ( for i being Nat st i in Seg n holds
y . i in ].(a . i),(b . i).] ) ) ) ) & ( for x being object holds
( x in I2 iff ex y being Element of REAL n st
( x = y & ( for i being Nat st i in Seg n holds
y . i in ].(a . i),(b . i).] ) ) ) ) implies I1 = I2 )
assume that
A20: for x being object holds
( x in I1 iff ex y being Element of REAL n st
( x = y & ( for i being Nat st i in Seg n holds
y . i in ].(a . i),(b . i).] ) ) ) and
A21: for x being object holds
( x in I2 iff ex y being Element of REAL n st
( x = y & ( for i being Nat st i in Seg n holds
y . i in ].(a . i),(b . i).] ) ) ) ; :: thesis: I1 = I2
thus I1 c= I2 :: according to XBOOLE_0:def 10 :: thesis: I2 c= I1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in I1 or x in I2 )
assume x in I1 ; :: thesis: x in I2
then consider y being Element of REAL n such that
A22: x = y and
A23: for i being Nat st i in Seg n holds
y . i in ].(a . i),(b . i).] by A20;
thus x in I2 by A21, A23, A22; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in I2 or x in I1 )
assume x in I2 ; :: thesis: x in I1
then consider y being Element of REAL n such that
A24: x = y and
A25: for i being Nat st i in Seg n holds
y . i in ].(a . i),(b . i).] by A21;
thus x in I1 by A24, A25, A20; :: thesis: verum