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 ;
A2: (y `) "\/" (Top L) = Top L ;
A3: y ` is_a_complement_of y by Def10;
then A4: (y `) "\/" y = Top L ;
(x "/\" y) ` is_a_complement_of x "/\" y by Def10;
then A5: ( ((x "/\" y) `) "\/" (x "/\" y) = Top L & ((x "/\" y) `) "/\" (x "/\" y) = Bottom L ) ;
A6: x ` is_a_complement_of x by Def10;
then A7: (x `) "\/" x = Top L ;
A8: (y `) "/\" y = Bottom L by A3;
A9: (x `) "/\" x = Bottom L by A6;
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
.= (Bottom L) "\/" (Bottom L)
.= Bottom L ;
((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 ;
then (x "/\" y) ` = (x `) "\/" (y `) by A10, A5, LATTICES:12;
hence x "/\" y = ((x `) "\/" (y `)) ` by Th32; :: thesis: verum