let L be non empty OrthoLattStr ; ( L is Ortholattice iff ( ( for a, b, c being Element of L holds (a "\/" b) "\/" c = (((c `) "/\" (b `)) `) "\/" a ) & ( for a, b being Element of L holds a = a "/\" (a "\/" b) ) & ( for a, b being Element of L holds a = a "\/" (b "/\" (b `)) ) ) )
thus
( L is Ortholattice implies ( ( for a, b, c being Element of L holds (a "\/" b) "\/" c = (((c `) "/\" (b `)) `) "\/" a ) & ( for a, b being Element of L holds a = a "/\" (a "\/" b) ) & ( for a, b being Element of L holds a = a "\/" (b "/\" (b `)) ) ) )
( ( for a, b, c being Element of L holds (a "\/" b) "\/" c = (((c `) "/\" (b `)) `) "\/" a ) & ( for a, b being Element of L holds a = a "/\" (a "\/" b) ) & ( for a, b being Element of L holds a = a "\/" (b "/\" (b `)) ) implies L is Ortholattice )proof
assume A1:
L is
Ortholattice
;
( ( for a, b, c being Element of L holds (a "\/" b) "\/" c = (((c `) "/\" (b `)) `) "\/" a ) & ( for a, b being Element of L holds a = a "/\" (a "\/" b) ) & ( for a, b being Element of L holds a = a "\/" (b "/\" (b `)) ) )
thus
for
a,
b,
c being
Element of
L holds
(a "\/" b) "\/" c = (((c `) "/\" (b `)) `) "\/" a
( ( for a, b being Element of L holds a = a "/\" (a "\/" b) ) & ( for a, b being Element of L holds a = a "\/" (b "/\" (b `)) ) )
thus
for
a,
b being
Element of
L holds
a = a "/\" (a "\/" b)
by A1, LATTICES:def 9;
for a, b being Element of L holds a = a "\/" (b "/\" (b `))
let a,
b be
Element of
L;
a = a "\/" (b "/\" (b `))
thus a "\/" (b "/\" (b `)) =
a "\/" (((b `) "\/" ((b `) `)) `)
by A1, ROBBINS1:def 23
.=
a "\/" (((b `) "\/" b) `)
by A1, ROBBINS3:def 6
.=
a "\/" ((b "\/" (b `)) `)
by A1, LATTICES:def 4
.=
a "\/" ((a "\/" (a `)) `)
by A1, ROBBINS3:def 7
.=
a "\/" ((((a `) `) "\/" (a `)) `)
by A1, ROBBINS3:def 6
.=
a "\/" ((a `) "/\" a)
by A1, ROBBINS1:def 23
.=
((a `) "/\" a) "\/" a
by A1, LATTICES:def 4
.=
a
by A1, LATTICES:def 8
;
verum
end;
assume A2:
for a, b, c being Element of L holds (a "\/" b) "\/" c = (((c `) "/\" (b `)) `) "\/" a
; ( ex a, b being Element of L st not a = a "/\" (a "\/" b) or ex a, b being Element of L st not a = a "\/" (b "/\" (b `)) or L is Ortholattice )
assume A3:
for a, b being Element of L holds a = a "/\" (a "\/" b)
; ( ex a, b being Element of L st not a = a "\/" (b "/\" (b `)) or L is Ortholattice )
assume A4:
for a, b being Element of L holds a = a "\/" (b "/\" (b `))
; L is Ortholattice
A5:
for a being Element of L holds a "/\" a = a
A6:
for a, b being Element of L holds a = (((b "/\" (b `)) `) `) "\/" a
A7:
for a being Element of L holds a "/\" (a `) = ((a "/\" (a `)) `) `
A8:
for a, b being Element of L holds a = (b "/\" (b `)) "\/" a
A9:
for a, b being Element of L holds a "\/" b = ((b `) "/\" (a `)) `
A10:
L is involutive
A11:
L is join-commutative
A12:
L is de_Morgan
A13:
L is meet-absorbing
A14:
L is join-associative
A15:
L is meet-associative
A16:
for a, b being Element of L holds a "/\" (a `) = b "/\" (b `)
A17:
L is with_Top
L is join-absorbing
by A3;
hence
L is Ortholattice
by A11, A14, A10, A12, A17, A15, A13; verum