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