let L be non empty Lattice-like involutive OrthoLattStr ; :: thesis: ( L is de_Morgan iff for a, b being Element of L st a [= b holds

b ` [= a ` )

thus ( L is de_Morgan implies for a, b being Element of L st a [= b holds

b ` [= a ` ) :: thesis: ( ( for a, b being Element of L st a [= b holds

b ` [= a ` ) implies L is de_Morgan )

b ` [= a ` ; :: thesis: L is de_Morgan

let x, y be Element of L; :: according to ROBBINS1:def 23 :: thesis: x "/\" y = ((x `) "\/" (y `)) `

((x `) "\/" (y `)) ` [= (y `) ` by A2, LATTICES:5;

then A3: ((x `) "\/" (y `)) ` [= y by ROBBINS3:def 6;

( x ` [= (x "/\" y) ` & y ` [= (x "/\" y) ` ) by A2, LATTICES:6;

then (x `) "\/" (y `) [= (x "/\" y) ` by FILTER_0:6;

then ((x "/\" y) `) ` [= ((x `) "\/" (y `)) ` by A2;

then A4: x "/\" y [= ((x `) "\/" (y `)) ` by ROBBINS3:def 6;

((x `) "\/" (y `)) ` [= (x `) ` by A2, LATTICES:5;

then ((x `) "\/" (y `)) ` [= x by ROBBINS3:def 6;

then ((x `) "\/" (y `)) ` [= x "/\" y by A3, FILTER_0:7;

hence x "/\" y = ((x `) "\/" (y `)) ` by A4, LATTICES:8; :: thesis: verum

b ` [= a ` )

thus ( L is de_Morgan implies for a, b being Element of L st a [= b holds

b ` [= a ` ) :: thesis: ( ( for a, b being Element of L st a [= b holds

b ` [= a ` ) implies L is de_Morgan )

proof

assume A2:
for a, b being Element of L st a [= b holds
assume A1:
L is de_Morgan
; :: thesis: for a, b being Element of L st a [= b holds

b ` [= a `

let a, b be Element of L; :: thesis: ( a [= b implies b ` [= a ` )

assume a [= b ; :: thesis: b ` [= a `

then a ` = (a "/\" b) ` by LATTICES:4

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

.= (b `) "\/" (a `) by ROBBINS3:def 6 ;

then (a `) "/\" (b `) = b ` by LATTICES:def 9;

hence b ` [= a ` by LATTICES:4; :: thesis: verum

end;b ` [= a `

let a, b be Element of L; :: thesis: ( a [= b implies b ` [= a ` )

assume a [= b ; :: thesis: b ` [= a `

then a ` = (a "/\" b) ` by LATTICES:4

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

.= (b `) "\/" (a `) by ROBBINS3:def 6 ;

then (a `) "/\" (b `) = b ` by LATTICES:def 9;

hence b ` [= a ` by LATTICES:4; :: thesis: verum

b ` [= a ` ; :: thesis: L is de_Morgan

let x, y be Element of L; :: according to ROBBINS1:def 23 :: thesis: x "/\" y = ((x `) "\/" (y `)) `

((x `) "\/" (y `)) ` [= (y `) ` by A2, LATTICES:5;

then A3: ((x `) "\/" (y `)) ` [= y by ROBBINS3:def 6;

( x ` [= (x "/\" y) ` & y ` [= (x "/\" y) ` ) by A2, LATTICES:6;

then (x `) "\/" (y `) [= (x "/\" y) ` by FILTER_0:6;

then ((x "/\" y) `) ` [= ((x `) "\/" (y `)) ` by A2;

then A4: x "/\" y [= ((x `) "\/" (y `)) ` by ROBBINS3:def 6;

((x `) "\/" (y `)) ` [= (x `) ` by A2, LATTICES:5;

then ((x `) "\/" (y `)) ` [= x by ROBBINS3:def 6;

then ((x `) "\/" (y `)) ` [= x "/\" y by A3, FILTER_0:7;

hence x "/\" y = ((x `) "\/" (y `)) ` by A4, LATTICES:8; :: thesis: verum