let L be bounded LATTICE; :: thesis: ( L is distributive & L is complemented implies for x being Element of L ex x9 being Element of L st
for y being Element of L holds
( (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 ) )
assume that
A1: L is distributive and
A2: L is complemented ; :: thesis: for x being Element of L ex x9 being Element of L st
for y being Element of L holds
( (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 )
let x be Element of L; :: thesis: ex x9 being Element of L st
for y being Element of L holds
( (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 )
consider x9 being Element of L such that
A3: x9 is_a_complement_of x by A2;
take x9 ; :: thesis: for y being Element of L holds
( (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 )
let y be Element of L; :: thesis: ( (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 )
(y "\/" x9) "/\" x = (x "/\" y) "\/" (x "/\" x9) by A1
.= (Bottom L) "\/" (x "/\" y) by A3
.= x "/\" y by Th3 ;
hence (y "\/" x9) "/\" x <= y by YELLOW_0:23; :: thesis: y <= (y "/\" x) "\/" x9
(y "/\" x) "\/" x9 = (x9 "\/" y) "/\" (x9 "\/" x) by A1, Th5
.= (x9 "\/" y) "/\" (Top L) by A3
.= x9 "\/" y by Th4 ;
hence y <= (y "/\" x) "\/" x9 by YELLOW_0:22; :: thesis: verum