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:18;
A2: (y `) "\/" (Top L) = Top L by LATTICES:18;
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:15
.= (Bottom L) "\/" (Bottom L) by LATTICES:15
.= Bottom L by LATTICES:14 ;
((x `) "\/" (y `)) "\/" (x "/\" y) = (((x `) "\/" (y `)) "\/" x) "/\" (((x `) "\/" (y `)) "\/" y) by LATTICES:11
.= (((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:17 ;
then (x "/\" y) ` = (x `) "\/" (y `) by A10, A5, LATTICES:12;
hence x "/\" y = ((x `) "\/" (y `)) ` by Th33; :: thesis: verum