let L be Ortholattice; :: thesis: for a being Element of L holds
( a "\/" (a ` ) = Top L & a "/\" (a ` ) = Bottom L )
let a be Element of L; :: thesis: ( a "\/" (a ` ) = Top L & a "/\" (a ` ) = Bottom L )
thus a "\/" (a ` ) = Top L :: thesis: a "/\" (a ` ) = Bottom L

proof

A: for b being Element of L holds (a "\/" (a ` )) "\/" b = a "\/" (a ` )

proof

let b be Element of L; :: thesis: (a "\/" (a ` )) "\/" b = a "\/" (a ` )
thus (a "\/" (a ` )) "\/" b = (b "\/" (b ` )) "\/" b by ROBBINS3:def 7
.= (b ` ) "\/" (b "\/" b) by LATTICES:def 5
.= (b ` ) "\/" b by LATTICES:17
.= a "\/" (a ` ) by ROBBINS3:def 7 ; :: thesis: verum

end;

for b being Element of L holds b "\/" (a "\/" (a ` )) = a "\/" (a ` ) by A;
hence a "\/" (a ` ) = Top L by A, LATTICES:def 17; :: thesis: verum

end;

A: for b being Element of L holds (a "/\" (a ` )) "/\" b = a "/\" (a ` )

proof

let b be Element of L; :: thesis: (a "/\" (a ` )) "/\" b = a "/\" (a ` )
thus (a "/\" (a ` )) "/\" b = (((a ` ) "\/" ((a ` ) ` )) ` ) "/\" b by ROBBINS1:def 23
.= (((b ` ) "\/" ((b ` ) ` )) ` ) "/\" b by ROBBINS3:def 7
.= (b "/\" (b ` )) "/\" b by ROBBINS1:def 23
.= (b ` ) "/\" (b "/\" b) by LATTICES:def 7
.= (b ` ) "/\" b by LATTICES:18
.= (((b ` ) ` ) "\/" (b ` )) ` by ROBBINS1:def 23
.= (((a ` ) ` ) "\/" (a ` )) ` by ROBBINS3:def 7
.= a "/\" (a ` ) by ROBBINS1:def 23 ; :: thesis: verum

end;

then for b being Element of L holds b "/\" (a "/\" (a ` )) = a "/\" (a ` ) ;
hence a "/\" (a ` ) = Bottom L by A, LATTICES:def 16; :: thesis: verum