let L be distributive bounded well-complemented preOrthoLattice; :: thesis: for x, y being Element of L holds x "/\" y = ((x ` ) "\/" (y ` )) `
let x, y be Element of L; :: thesis: x "/\" y = ((x ` ) "\/" (y ` )) `
A1: (x ` ) "\/" (Top L) = Top L by LATTICES:44;
A2: (y ` ) "\/" (Top L) = Top L by LATTICES:44;
A3: y ` is_a_complement_of y by Def10;
then A4: (y ` ) "\/" y = Top L by LATTICES:def 18;
(x "/\" y) ` is_a_complement_of x "/\" y by Def10;
then A5: ( ((x "/\" y) ` ) "\/" (x "/\" y) = Top L & ((x "/\" y) ` ) "/\" (x "/\" y) = Bottom L ) by LATTICES:def 18;
A6: x ` is_a_complement_of x by Def10;
then A7: (x ` ) "\/" x = Top L by LATTICES:def 18;
A8: (y ` ) "/\" y = Bottom L by A3, LATTICES:def 18;
A9: (x ` ) "/\" x = Bottom L by A6, LATTICES:def 18;
A10: ((x ` ) "\/" (y ` )) "/\" (x "/\" y) = ((x "/\" y) "/\" (x ` )) "\/" ((x "/\" y) "/\" (y ` )) by LATTICES:def 11
.= (y "/\" (x "/\" (x ` ))) "\/" ((x "/\" y) "/\" (y ` )) by LATTICES:def 7
.= (y "/\" (Bottom L)) "\/" (x "/\" (y "/\" (y ` ))) by A9, LATTICES:def 7
.= (Bottom L) "\/" (x "/\" (Bottom L)) by A8, LATTICES:40
.= (Bottom L) "\/" (Bottom L) by LATTICES:40
.= Bottom L by LATTICES:39 ;
((x ` ) "\/" (y ` )) "\/" (x "/\" y) = (((x ` ) "\/" (y ` )) "\/" x) "/\" (((x ` ) "\/" (y ` )) "\/" y) by LATTICES:31
.= (((y ` ) "\/" (x ` )) "\/" x) "/\" (Top L) by A4, A1, LATTICES:def 5
.= (Top L) "/\" (Top L) by A7, A2, LATTICES:def 5
.= Top L by LATTICES:43 ;
then (x "/\" y) ` = (x ` ) "\/" (y ` ) by A10, A5, LATTICES:32;
hence x "/\" y = ((x ` ) "\/" (y ` )) ` by Th33; :: thesis: verum