let L be Boolean Lattice; :: thesis: for x being Element of L holds x ` = x *
let x be Element of L; :: thesis: x ` = x *
a1: x * [= x `

proof

(x *) "/\" x = Bottom L by ThD;
hence x * [= x ` by LATTICES:25; :: thesis: verum

end;

x ` [= x *

proof

a1: (x `) "/\" x = Bottom L by LATTICES:20;
x * is_a_pseudocomplement_of x by def3;
hence x ` [= x * by a1; :: thesis: verum

end;

hence x ` = x * by a1, LATTICES:8; :: thesis: verum