assume
x in { d where d is Element of L : ( d in D & d [= x ) }
; :: thesis: contradiction then
ex x9 being Element of L st ( x9 = x & x9 in D & x9 [= x )
; hence
contradiction
byA4; :: thesis: verum
end;
for u being object st u in { d where d is Element of L : ( d in D & d [= x ) } holds u in { d where d is Element of L : ( d [= x & d <> x ) }