let a be Element of L; :: thesis: a ="\/" ( { d where d is Element of L : ( d in D & d [= a ) } ,L) set X = { d where d is Element of L : ( d in D & d [= a ) } ; consider D9 being Subset of D such that A3:
a ="\/" (D9,L)
byA2;
for x being object st x in D9 holds x in { d where d is Element of L : ( d in D & d [= a ) }