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
A7: for x being Element of L holds
( x in S1 iff ex y being Element of L st
( y <= x & y in X ) ) and
A8: 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 S1 or x in S2 )
assume A9: 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 A7, A9;
hence x in S2 by A8; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in S2 or x in S1 )
assume A10: 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 A8, A10;
hence x in S1 by A7; :: thesis: verum