let L be Boolean Lattice; :: thesis: L is pseudocomplemented
L is pseudocomplemented

proof

let x be Element of L; :: according to LATSTONE:def 2 :: thesis: ex y being Element of L st y is_a_pseudocomplement_of x
take y = x ` ; :: thesis: y is_a_pseudocomplement_of x
for z being Element of L st x "/\" z = Bottom L holds
z [= y

proof

let z be Element of L; :: thesis: ( x "/\" z = Bottom L implies z [= y )
assume E1: x "/\" z = Bottom L ; :: thesis: z [= y
z = z "/\" (Top L)
.= z "/\" (x "\/" y) by LATTICES:21
.= (z "/\" x) "\/" (z "/\" y) by LATTICES:def 11
.= z "/\" y by E1 ;
hence z [= y by LATTICES:4; :: thesis: verum

end;

hence y is_a_pseudocomplement_of x by LATTICES:20; :: thesis: verum

end;

hence L is pseudocomplemented ; :: thesis: verum