let x, y be Subset of L; :: thesis: ( ( for c being Element of L holds
( c in x iff ( a <= c & c <= b ) ) ) & ( for c being Element of L holds
( c in y iff ( a <= c & c <= b ) ) ) implies x = y )
assume that
A3: for c being Element of L holds
( c in x iff ( a <= c & c <= b ) ) and
A4: for c being Element of L holds
( c in y iff ( a <= c & c <= b ) ) ; :: thesis: x = y

A5: now

let c1 be set ; :: thesis: ( c1 in x implies c1 in y )
assume A6: c1 in x ; :: thesis: c1 in y
then reconsider c = c1 as Element of L ;
( c in x iff ( a <= c & c <= b ) ) by A3;
hence c1 in y by A4, A6; :: thesis: verum

end;

now

let c1 be set ; :: thesis: ( c1 in y implies c1 in x )
assume A7: c1 in y ; :: thesis: c1 in x
then reconsider c = c1 as Element of L ;
( c in y iff ( a <= c & c <= b ) ) by A4;
hence c1 in x by A3, A7; :: thesis: verum

end;

then ( x c= y & y c= x ) by A5, TARSKI:def 3;
hence x = y by XBOOLE_0:def 10; :: thesis: verum