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 )

then a "/\" (a `) = a ;

then a [= a ` by LATTICES:4;

hence a _|_ a ; :: thesis: verum

( 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 = Bottom L
; :: thesis: a _|_ a
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;then a [= a ` ;

then a "/\" (a `) = a by LATTICES:4;

hence a = Bottom L by Th2; :: thesis: verum

then a "/\" (a `) = a ;

then a [= a ` by LATTICES:4;

hence a _|_ a ; :: thesis: verum