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 )
proof
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;
assume A2: for a, b being Element of L st a [= b holds
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