assume
x in { d where d is Element of L : ( d in D & x [= d ) }
; :: thesis: contradiction then
ex x9 being Element of L st ( x9 = x & x9 in D & x [= x9 )
; hence
contradiction
byA4; :: thesis: verum
end;
for u being object st u in { d where d is Element of L : ( d in D & x [= d ) } holds u in { d where d is Element of L : ( x [= d & d <> x ) }
then { d where d is Element of L : ( d in D & x [= d ) } c= { d where d is Element of L : ( x [= d & d <> x ) }
; then "/\" ( { d where d is Element of L : ( x [= d & d <> x ) } ,L) [="/\" ( { d where d is Element of L : ( d in D & x [= d ) } ,L)
byLATTICE3:45; then A7:
"/\" ( { d where d is Element of L : ( x [= d & d <> x ) } ,L) [= x
byA1, Th24;
for q being Element of L st q in { d where d is Element of L : ( x [= d & d <> x ) } holds x [= q