let L be sup-Semilattice; :: thesis: for x being Element of L holds
( x is co-prime iff for A being non empty finite Subset of L st x <= sup A holds
ex a being Element of L st
( a in A & x <= a ) )
let x be Element of L; :: thesis: ( x is co-prime iff for A being non empty finite Subset of L st x <= sup A holds
ex a being Element of L st
( a in A & x <= a ) )
thus ( x is co-prime implies for A being non empty finite Subset of L st x <= sup A holds
ex a being Element of L st
( a in A & x <= a ) ) :: thesis: ( ( for A being non empty finite Subset of L st x <= sup A holds
ex a being Element of L st
( a in A & x <= a ) ) implies x is co-prime )

proof

assume x is co-prime ; :: thesis: for A being non empty finite Subset of L st x <= sup A holds
ex a being Element of L st
( a in A & x <= a )
then A1: x ~ is prime ;
let A be non empty finite Subset of L; :: thesis: ( x <= sup A implies ex a being Element of L st
( a in A & x <= a ) )
reconsider A1 = A as non empty finite Subset of (L ~) ;
assume x <= sup A ; :: thesis: ex a being Element of L st
( a in A & x <= a )
then A2: x ~ >= (sup A) ~ by LATTICE3:9;
A3: ex_sup_of A,L by YELLOW_0:54;
then "\/" (A,L) is_>=_than A by YELLOW_0:def 9;
then A4: ("\/" (A,L)) ~ is_<=_than A by YELLOW_7:8;

A5: now :: thesis: for y being Element of (L ~) st y is_<=_than A holds
y <= ("\/" (A,L)) ~

let y be Element of (L ~); :: thesis: ( y is_<=_than A implies y <= ("\/" (A,L)) ~ )
assume y is_<=_than A ; :: thesis: y <= ("\/" (A,L)) ~
then ~ y is_>=_than A by YELLOW_7:9;
then ~ y >= "\/" (A,L) by A3, YELLOW_0:def 9;
hence y <= ("\/" (A,L)) ~ by YELLOW_7:2; :: thesis: verum

end;

ex_inf_of A,L ~ by A3, YELLOW_7:10;
then (sup A) ~ = inf A1 by A4, A5, YELLOW_0:def 10;
then consider a being Element of (L ~) such that
A6: ( a in A1 & x ~ >= a ) by A1, A2, Th22;
take ~ a ; :: thesis: ( ~ a in A & x <= ~ a )
thus ( ~ a in A & x <= ~ a ) by A6, YELLOW_7:2; :: thesis: verum

end;

thus ( ( for A being non empty finite Subset of L st x <= sup A holds
ex a being Element of L st
( a in A & x <= a ) ) implies x is co-prime ) :: thesis: verum

proof

assume A7: for A being non empty finite Subset of L st x <= sup A holds
ex a being Element of L st
( a in A & x <= a ) ; :: thesis: x is co-prime

now :: thesis: for a, b being Element of (L ~) holds
( not a "/\" b <= x ~ or a <= x ~ or b <= x ~ )

let a, b be Element of (L ~); :: thesis: ( not a "/\" b <= x ~ or a <= x ~ or b <= x ~ )
set A = {(~ a),(~ b)};
assume a "/\" b <= x ~ ; :: thesis: ( a <= x ~ or b <= x ~ )
then x <= ~ (a "/\" b) by YELLOW_7:2;
then ( sup {(~ a),(~ b)} = (~ a) "\/" (~ b) & x <= (~ a) "\/" (~ b) ) by YELLOW_0:41, YELLOW_7:24;
then consider l being Element of L such that
A8: l in {(~ a),(~ b)} and
A9: x <= l by A7;
( l = ~ a or l = ~ b ) by A8, TARSKI:def 2;
hence ( a <= x ~ or b <= x ~ ) by A9, YELLOW_7:2; :: thesis: verum

end;

then x ~ is prime ;
hence x is co-prime ; :: thesis: verum

end;