let x, y be Subset of L; ( ( 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 ) )
; x = y
then A5:
y c= x
;
then
x c= y
;
hence
x = y
by A5; verum