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 `)
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
.= a "\/" (a `) by ROBBINS3:def 7 ; :: thesis: verum
end;
then for b being Element of L holds b "\/" (a "\/" (a `)) = 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 `)
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
.= (((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 A2, LATTICES:def 16; :: thesis: verum