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 :: thesis: for c1 being object st c1 in y holds
c1 in x

let c1 be object ; :: 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 ;

now :: thesis: for c1 being object st c1 in x holds
c1 in y

let c1 be object ; :: 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 ;
hence x = y by A5; :: thesis: verum