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 ` )) `
x ` is_a_complement_of x by Def10;
then A1: ( (x ` ) "\/" x = Top L & (x ` ) "/\" x = Bottom L ) by LATTICES:def 18;
y ` is_a_complement_of y by Def10;
then A2: ( (y ` ) "\/" y = Top L & (y ` ) "/\" y = Bottom L ) by LATTICES:def 18;
A3: ((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 A1, LATTICES:def 7
.= (Bottom L) "\/" (x "/\" (Bottom L)) by A2, LATTICES:40
.= (Bottom L) "\/" (Bottom L) by LATTICES:40
.= Bottom L by LATTICES:39 ;
A4: (x ` ) "\/" (Top L) = Top L by LATTICES:44;
A5: (y ` ) "\/" (Top L) = Top L by LATTICES:44;
A6: ((x ` ) "\/" (y ` )) "\/" (x "/\" y) = (((x ` ) "\/" (y ` )) "\/" x) "/\" (((x ` ) "\/" (y ` )) "\/" y) by LATTICES:31
.= (((y ` ) "\/" (x ` )) "\/" x) "/\" (Top L) by A2, A4, LATTICES:def 5
.= (Top L) "/\" (Top L) by A1, A5, LATTICES:def 5
.= Top L by LATTICES:43 ;
(x "/\" y) ` is_a_complement_of x "/\" y by Def10;
then ( ((x "/\" y) ` ) "\/" (x "/\" y) = Top L & ((x "/\" y) ` ) "/\" (x "/\" y) = Bottom L ) by LATTICES:def 18;
then (x "/\" y) ` = (x ` ) "\/" (y ` ) by A3, A6, LATTICES:32;
hence x "/\" y = ((x ` ) "\/" (y ` )) ` by Th33; :: thesis: verum