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

hence x = y by A5; :: thesis: verum

( 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

then A5:
y c= x
;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;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

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

c1 in y

then
x c= y
;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;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

hence x = y by A5; :: thesis: verum