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

( 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