let L be Lattice; :: thesis: for a, b being Element of L holds
( b in PseudoComplements a iff b "/\" a = Bottom L )
let a, b be Element of L; :: thesis: ( b in PseudoComplements a iff b "/\" a = Bottom L )

hereby :: thesis: ( b "/\" a = Bottom L implies b in PseudoComplements a )

assume b in PseudoComplements a ; :: thesis: b "/\" a = Bottom L
then consider x being Element of L such that
A1: ( b = x & a "/\" x = Bottom L ) ;
thus b "/\" a = Bottom L by A1; :: thesis: verum

end;

assume b "/\" a = Bottom L ; :: thesis: b in PseudoComplements a
hence b in PseudoComplements a ; :: thesis: verum