let L be Ortholattice; :: thesis: for a being Element of L holds
( a _|_ a iff a = Bottom L )
let a be Element of L; :: thesis: ( a _|_ a iff a = Bottom L )
thus ( a _|_ a implies a = Bottom L ) :: thesis: ( a = Bottom L implies a _|_ a )
proof
assume a _|_ a ; :: thesis: a = Bottom L
then a [= a ` ;
then a "/\" (a `) = a by LATTICES:4;
hence a = Bottom L by Th2; :: thesis: verum
end;
assume a = Bottom L ; :: thesis: a _|_ a
then a "/\" (a `) = a ;
then a [= a ` by LATTICES:4;
hence a _|_ a ; :: thesis: verum