let L be complete LATTICE; :: thesis: ( L is distributive & L is continuous & L ~ is continuous implies for l being Element of L ex X being Subset of L st
( l = sup X & ( for x being Element of L st x in X holds
x is co-prime ) ) )
assume that
A1: ( L is distributive & L is continuous ) and
A2: L ~ is continuous ; :: thesis: for l being Element of L ex X being Subset of L st
( l = sup X & ( for x being Element of L st x in X holds
x is co-prime ) )
let l be Element of L; :: thesis: ex X being Subset of L st
( l = sup X & ( for x being Element of L st x in X holds
x is co-prime ) )
reconsider L = L as distributive complete continuous LATTICE by A1;
reconsider l1 = l as Element of (L ~) ;
PRIME (L ~) is order-generating by A2, Th35;
then consider Y being Subset of (PRIME (L ~)) such that
A3: l1 = "/\" (Y,(L ~)) by Th15;
reconsider Y = Y as Subset of L by XBOOLE_1:1;
A4: for x being Element of L st x in Y holds
x is co-prime by Def7;
ex_sup_of Y,L by YELLOW_0:17;
then "\/" (Y,L) = "/\" (Y,(L ~)) by YELLOW_7:12;
hence ex X being Subset of L st
( l = sup X & ( for x being Element of L st x in X holds
x is co-prime ) ) by A3, A4; :: thesis: verum