let L be non empty join-commutative meet-commutative well-complemented OrthoLattStr ; :: thesis: for x being Element of L holds
( x + (x `) = Top L & x "/\" (x `) = Bottom L )
let x be Element of L; :: thesis: ( x + (x `) = Top L & x "/\" (x `) = Bottom L )
A1: x ` is_a_complement_of x by Def10;
hence x + (x `) = Top L ; :: thesis: x "/\" (x `) = Bottom L
thus x "/\" (x `) = Bottom L by A1; :: thesis: verum