let L be non empty OrthoLattStr ; :: thesis: ( 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 `)) ) ) ) :: thesis: ( ( 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 )

assume A3: for a, b being Element of L holds a = a "/\" (a "\/" b) ; :: thesis: ( 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 `)) ; :: thesis: L is Ortholattice

A5: for a being Element of L holds a "/\" a = a

hence L is Ortholattice by A11, A14, A10, A12, A17, A15, A13; :: thesis: verum

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 `)) ) ) ) :: thesis: ( ( 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 A2:
for a, b, c being Element of L holds (a "\/" b) "\/" c = (((c `) "/\" (b `)) `) "\/" a
; :: thesis: ( 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 A1:
L is Ortholattice
; :: thesis: ( ( 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 :: thesis: ( ( for a, b being Element of L holds a = a "/\" (a "\/" b) ) & ( for a, b being Element of L holds a = a "\/" (b "/\" (b `)) ) )

let a, b be Element of L; :: thesis: 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 ; :: thesis: verum

end;thus for a, b, c being Element of L holds (a "\/" b) "\/" c = (((c `) "/\" (b `)) `) "\/" a :: thesis: ( ( for a, b being Element of L holds a = a "/\" (a "\/" b) ) & ( for a, b being Element of L holds a = a "\/" (b "/\" (b `)) ) )

proof

thus
for a, b being Element of L holds a = a "/\" (a "\/" b)
by A1, LATTICES:def 9; :: thesis: for a, b being Element of L holds a = a "\/" (b "/\" (b `))
let a, b, c be Element of L; :: thesis: (a "\/" b) "\/" c = (((c `) "/\" (b `)) `) "\/" a

(((c `) "/\" (b `)) `) "\/" a = (((((c `) `) "\/" ((b `) `)) `) `) "\/" a by A1, ROBBINS1:def 23;

then (((c `) "/\" (b `)) `) "\/" a = (((c "\/" ((b `) `)) `) `) "\/" a by A1, ROBBINS3:def 6;

then (((c `) "/\" (b `)) `) "\/" a = (((c "\/" b) `) `) "\/" a by A1, ROBBINS3:def 6;

then (((c `) "/\" (b `)) `) "\/" a = (c "\/" b) "\/" a by A1, ROBBINS3:def 6;

then (((c `) "/\" (b `)) `) "\/" a = a "\/" (c "\/" b) by A1, LATTICES:def 4;

then (((c `) "/\" (b `)) `) "\/" a = c "\/" (a "\/" b) by A1, ROBBINS3:def 1;

hence (a "\/" b) "\/" c = (((c `) "/\" (b `)) `) "\/" a by A1, LATTICES:def 4; :: thesis: verum

end;(((c `) "/\" (b `)) `) "\/" a = (((((c `) `) "\/" ((b `) `)) `) `) "\/" a by A1, ROBBINS1:def 23;

then (((c `) "/\" (b `)) `) "\/" a = (((c "\/" ((b `) `)) `) `) "\/" a by A1, ROBBINS3:def 6;

then (((c `) "/\" (b `)) `) "\/" a = (((c "\/" b) `) `) "\/" a by A1, ROBBINS3:def 6;

then (((c `) "/\" (b `)) `) "\/" a = (c "\/" b) "\/" a by A1, ROBBINS3:def 6;

then (((c `) "/\" (b `)) `) "\/" a = a "\/" (c "\/" b) by A1, LATTICES:def 4;

then (((c `) "/\" (b `)) `) "\/" a = c "\/" (a "\/" b) by A1, ROBBINS3:def 1;

hence (a "\/" b) "\/" c = (((c `) "/\" (b `)) `) "\/" a by A1, LATTICES:def 4; :: thesis: verum

let a, b be Element of L; :: thesis: 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 ; :: thesis: verum

assume A3: for a, b being Element of L holds a = a "/\" (a "\/" b) ; :: thesis: ( 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 `)) ; :: thesis: L is Ortholattice

A5: for a being Element of L holds a "/\" a = a

proof

A6:
for a, b being Element of L holds a = (((b "/\" (b `)) `) `) "\/" a
let a be Element of L; :: thesis: a "/\" a = a

thus a "/\" a = a "/\" (a "\/" (a "/\" (a `))) by A4

.= a by A3 ; :: thesis: verum

end;thus a "/\" a = a "/\" (a "\/" (a "/\" (a `))) by A4

.= a by A3 ; :: thesis: verum

proof

A7:
for a being Element of L holds a "/\" (a `) = ((a "/\" (a `)) `) `
let a, b be Element of L; :: thesis: a = (((b "/\" (b `)) `) `) "\/" a

set x = b "/\" (b `);

(a "\/" (b "/\" (b `))) "\/" (b "/\" (b `)) = ((((b "/\" (b `)) `) "/\" ((b "/\" (b `)) `)) `) "\/" a by A2;

then (a "\/" (b "/\" (b `))) "\/" (b "/\" (b `)) = (((b "/\" (b `)) `) `) "\/" a by A5;

then a "\/" (b "/\" (b `)) = (((b "/\" (b `)) `) `) "\/" a by A4;

hence a = (((b "/\" (b `)) `) `) "\/" a by A4; :: thesis: verum

end;set x = b "/\" (b `);

(a "\/" (b "/\" (b `))) "\/" (b "/\" (b `)) = ((((b "/\" (b `)) `) "/\" ((b "/\" (b `)) `)) `) "\/" a by A2;

then (a "\/" (b "/\" (b `))) "\/" (b "/\" (b `)) = (((b "/\" (b `)) `) `) "\/" a by A5;

then a "\/" (b "/\" (b `)) = (((b "/\" (b `)) `) `) "\/" a by A4;

hence a = (((b "/\" (b `)) `) `) "\/" a by A4; :: thesis: verum

proof

A8:
for a, b being Element of L holds a = (b "/\" (b `)) "\/" a
let a be Element of L; :: thesis: a "/\" (a `) = ((a "/\" (a `)) `) `

set x = a "/\" (a `);

thus a "/\" (a `) = (((a "/\" (a `)) `) `) "\/" (a "/\" (a `)) by A6

.= ((a "/\" (a `)) `) ` by A4 ; :: thesis: verum

end;set x = a "/\" (a `);

thus a "/\" (a `) = (((a "/\" (a `)) `) `) "\/" (a "/\" (a `)) by A6

.= ((a "/\" (a `)) `) ` by A4 ; :: thesis: verum

proof

A9:
for a, b being Element of L holds a "\/" b = ((b `) "/\" (a `)) `
let a, b be Element of L; :: thesis: a = (b "/\" (b `)) "\/" a

a = (((b "/\" (b `)) `) `) "\/" a by A6;

hence a = (b "/\" (b `)) "\/" a by A7; :: thesis: verum

end;a = (((b "/\" (b `)) `) `) "\/" a by A6;

hence a = (b "/\" (b `)) "\/" a by A7; :: thesis: verum

proof

A10:
L is involutive
let a, b be Element of L; :: thesis: a "\/" b = ((b `) "/\" (a `)) `

set x = a "/\" (a `);

((a "/\" (a `)) "\/" a) "\/" b = (((b `) "/\" (a `)) `) "\/" (a "/\" (a `)) by A2;

hence a "\/" b = (((b `) "/\" (a `)) `) "\/" (a "/\" (a `)) by A8

.= ((b `) "/\" (a `)) ` by A4 ;

:: thesis: verum

end;set x = a "/\" (a `);

((a "/\" (a `)) "\/" a) "\/" b = (((b `) "/\" (a `)) `) "\/" (a "/\" (a `)) by A2;

hence a "\/" b = (((b `) "/\" (a `)) `) "\/" (a "/\" (a `)) by A8

.= ((b `) "/\" (a `)) ` by A4 ;

:: thesis: verum

proof

A11:
L is join-commutative
let a be Element of L; :: according to ROBBINS3:def 6 :: thesis: (a `) ` = a

( a ` = (a `) "/\" ((a `) "\/" a) & (a `) "\/" a = ((a `) "/\" ((a `) `)) ` ) by A3, A9;

hence (a `) ` = ((a `) "/\" ((a `) `)) "\/" a by A9

.= a by A8 ;

:: thesis: verum

end;( a ` = (a `) "/\" ((a `) "\/" a) & (a `) "\/" a = ((a `) "/\" ((a `) `)) ` ) by A3, A9;

hence (a `) ` = ((a `) "/\" ((a `) `)) "\/" a by A9

.= a by A8 ;

:: thesis: verum

proof

A12:
L is de_Morgan
let a, b be Element of L; :: according to LATTICES:def 4 :: thesis: a "\/" b = b "\/" a

set x = a "/\" (a `);

(a "/\" (a `)) "\/" b = ((b `) "/\" ((a "/\" (a `)) `)) ` by A9;

hence b "\/" a = (((b `) "/\" ((a "/\" (a `)) `)) `) "\/" a by A8

.= (a "\/" (a "/\" (a `))) "\/" b by A2

.= a "\/" b by A4 ;

:: thesis: verum

end;set x = a "/\" (a `);

(a "/\" (a `)) "\/" b = ((b `) "/\" ((a "/\" (a `)) `)) ` by A9;

hence b "\/" a = (((b `) "/\" ((a "/\" (a `)) `)) `) "\/" a by A8

.= (a "\/" (a "/\" (a `))) "\/" b by A2

.= a "\/" b by A4 ;

:: thesis: verum

proof

A13:
L is meet-absorbing
let a, b be Element of L; :: according to ROBBINS1:def 23 :: thesis: a "/\" b = ((a `) "\/" (b `)) `

thus ((a `) "\/" (b `)) ` = ((b `) "\/" (a `)) ` by A11

.= ((((a `) `) "/\" ((b `) `)) `) ` by A9

.= ((a `) `) "/\" ((b `) `) by A10

.= ((a `) `) "/\" b by A10

.= a "/\" b by A10 ; :: thesis: verum

end;thus ((a `) "\/" (b `)) ` = ((b `) "\/" (a `)) ` by A11

.= ((((a `) `) "/\" ((b `) `)) `) ` by A9

.= ((a `) `) "/\" ((b `) `) by A10

.= ((a `) `) "/\" b by A10

.= a "/\" b by A10 ; :: thesis: verum

proof

A14:
L is join-associative
let a, b be Element of L; :: according to LATTICES:def 8 :: thesis: (a "/\" b) "\/" b = b

thus (a "/\" b) "\/" b = ((b `) "/\" ((a "/\" b) `)) ` by A9

.= ((b `) "/\" ((((a `) "\/" (b `)) `) `)) ` by A12

.= ((b `) "/\" ((a `) "\/" (b `))) ` by A10

.= ((b `) "/\" ((b `) "\/" (a `))) ` by A11

.= (b `) ` by A3

.= b by A10 ; :: thesis: verum

end;thus (a "/\" b) "\/" b = ((b `) "/\" ((a "/\" b) `)) ` by A9

.= ((b `) "/\" ((((a `) "\/" (b `)) `) `)) ` by A12

.= ((b `) "/\" ((a `) "\/" (b `))) ` by A10

.= ((b `) "/\" ((b `) "\/" (a `))) ` by A11

.= (b `) ` by A3

.= b by A10 ; :: thesis: verum

proof

A15:
L is meet-associative
let a, b, c be Element of L; :: according to LATTICES:def 5 :: thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c

thus (a "\/" b) "\/" c = (((c `) "/\" (b `)) `) "\/" a by A2

.= (b "\/" c) "\/" a by A9

.= a "\/" (b "\/" c) by A11 ; :: thesis: verum

end;thus (a "\/" b) "\/" c = (((c `) "/\" (b `)) `) "\/" a by A2

.= (b "\/" c) "\/" a by A9

.= a "\/" (b "\/" c) by A11 ; :: thesis: verum

proof

A16:
for a, b being Element of L holds a "/\" (a `) = b "/\" (b `)
let a, b, c be Element of L; :: according to LATTICES:def 7 :: thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c

thus a "/\" (b "/\" c) = ((a `) "\/" ((b "/\" c) `)) ` by A12

.= ((a `) "\/" ((((b `) "\/" (c `)) `) `)) ` by A12

.= ((a `) "\/" ((b `) "\/" (c `))) ` by A10

.= (((a `) "\/" (b `)) "\/" (c `)) ` by A14

.= (((((a `) "\/" (b `)) `) `) "\/" (c `)) ` by A10

.= (((a "/\" b) `) "\/" (c `)) ` by A12

.= (a "/\" b) "/\" c by A12 ; :: thesis: verum

end;thus a "/\" (b "/\" c) = ((a `) "\/" ((b "/\" c) `)) ` by A12

.= ((a `) "\/" ((((b `) "\/" (c `)) `) `)) ` by A12

.= ((a `) "\/" ((b `) "\/" (c `))) ` by A10

.= (((a `) "\/" (b `)) "\/" (c `)) ` by A14

.= (((((a `) "\/" (b `)) `) `) "\/" (c `)) ` by A10

.= (((a "/\" b) `) "\/" (c `)) ` by A12

.= (a "/\" b) "/\" c by A12 ; :: thesis: verum

proof

A17:
L is with_Top
let a, b be Element of L; :: thesis: a "/\" (a `) = b "/\" (b `)

a "/\" (a `) = (a "/\" (a `)) "\/" (b "/\" (b `)) by A4;

hence a "/\" (a `) = b "/\" (b `) by A8; :: thesis: verum

end;a "/\" (a `) = (a "/\" (a `)) "\/" (b "/\" (b `)) by A4;

hence a "/\" (a `) = b "/\" (b `) by A8; :: thesis: verum

proof

L is join-absorbing
by A3;
let a, b be Element of L; :: according to ROBBINS3:def 7 :: thesis: a "\/" (a `) = b "\/" (b `)

((a `) "/\" ((a `) `)) ` = ((b `) "/\" ((b `) `)) ` by A16;

then ((a `) "/\" ((a `) `)) ` = (b `) "\/" b by A9;

then (a `) "\/" a = (b `) "\/" b by A9;

then (a `) "\/" a = b "\/" (b `) by A11;

hence a "\/" (a `) = b "\/" (b `) by A11; :: thesis: verum

end;((a `) "/\" ((a `) `)) ` = ((b `) "/\" ((b `) `)) ` by A16;

then ((a `) "/\" ((a `) `)) ` = (b `) "\/" b by A9;

then (a `) "\/" a = (b `) "\/" b by A9;

then (a `) "\/" a = b "\/" (b `) by A11;

hence a "\/" (a `) = b "\/" (b `) by A11; :: thesis: verum

hence L is Ortholattice by A11, A14, A10, A12, A17, A15, A13; :: thesis: verum