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 )

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

hence a "\/" (a `) = Top L by A1, LATTICES:def 17; :: thesis: a "/\" (a `) = Bottom L

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

hence a "/\" (a `) = Bottom L by A2, LATTICES:def 16; :: thesis: verum

( a "\/" (a `) = Top L & a "/\" (a `) = Bottom L )

let a be Element of L; :: thesis: ( a "\/" (a `) = Top L & a "/\" (a `) = Bottom L )

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

proof

then
for b being Element of L holds b "\/" (a "\/" (a `)) = a "\/" (a `)
;
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

.= a "\/" (a `) by ROBBINS3:def 7 ; :: thesis: verum

end;thus (a "\/" (a `)) "\/" b = (b "\/" (b `)) "\/" b by ROBBINS3:def 7

.= (b `) "\/" (b "\/" b) by LATTICES:def 5

.= (b `) "\/" b

.= a "\/" (a `) by ROBBINS3:def 7 ; :: thesis: verum

hence a "\/" (a `) = Top L by A1, LATTICES:def 17; :: thesis: a "/\" (a `) = Bottom L

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

proof

then
for b being Element of L holds b "/\" (a "/\" (a `)) = a "/\" (a `)
;
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

.= (((b `) `) "\/" (b `)) ` by ROBBINS1:def 23

.= (((a `) `) "\/" (a `)) ` by ROBBINS3:def 7

.= a "/\" (a `) by ROBBINS1:def 23 ; :: thesis: verum

end;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

.= (((b `) `) "\/" (b `)) ` by ROBBINS1:def 23

.= (((a `) `) "\/" (a `)) ` by ROBBINS3:def 7

.= a "/\" (a `) by ROBBINS1:def 23 ; :: thesis: verum

hence a "/\" (a `) = Bottom L by A2, LATTICES:def 16; :: thesis: verum