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

proof

let x be set ; :: 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;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in S2 or x in 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