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
A2: for c being Element of L holds
( c in x iff ( a <= c & c <= b ) ) and
A3: for c being Element of L holds
( c in y iff ( a <= c & c <= b ) ) ; :: thesis: x = y

now

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

end;

then A5: y c= x by TARSKI:def 3;

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 A2;
hence c1 in y by A3, A6; :: thesis: verum

end;

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