let S1, S2 be Subset of L; :: thesis: ( ( for x being Element of L holds

( x in S1 iff ex y being Element of L st

( y >= x & y in X ) ) ) & ( for x being Element of L holds

( x in S2 iff ex y being Element of L st

( y >= x & y in X ) ) ) implies S1 = S2 )

assume that

A2: for x being Element of L holds

( x in S1 iff ex y being Element of L st

( y >= x & y in X ) ) and

A3: for x being Element of L holds

( x in S2 iff ex y being Element of L st

( y >= x & y in X ) ) ; :: thesis: S1 = S2

thus S1 c= S2 :: according to XBOOLE_0:def 10 :: thesis: S2 c= S1

assume A5: x in S2 ; :: thesis: x in S1

then reconsider x = x as Element of L ;

ex y being Element of L st

( y >= x & y in X ) by A3, A5;

hence x in S1 by A2; :: thesis: verum

( x in S1 iff ex y being Element of L st

( y >= x & y in X ) ) ) & ( for x being Element of L holds

( x in S2 iff ex y being Element of L st

( y >= x & y in X ) ) ) implies S1 = S2 )

assume that

A2: for x being Element of L holds

( x in S1 iff ex y being Element of L st

( y >= x & y in X ) ) and

A3: for x being Element of L holds

( x in S2 iff ex y being Element of L st

( y >= x & y in X ) ) ; :: thesis: S1 = S2

thus S1 c= S2 :: according to XBOOLE_0:def 10 :: thesis: S2 c= S1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in S2 or x in S1 )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in S1 or x in S2 )

assume A4: x in S1 ; :: thesis: x in S2

then reconsider x = x as Element of L ;

ex y being Element of L st

( y >= x & y in X ) by A2, A4;

hence x in S2 by A3; :: thesis: verum

end;assume A4: x in S1 ; :: thesis: x in S2

then reconsider x = x as Element of L ;

ex y being Element of L st

( y >= x & y in X ) by A2, A4;

hence x in S2 by A3; :: thesis: verum

assume A5: x in S2 ; :: thesis: x in S1

then reconsider x = x as Element of L ;

ex y being Element of L st

( y >= x & y in X ) by A3, A5;

hence x in S1 by A2; :: thesis: verum