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 by Def8;
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 ) )
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;
reconsider A1 = A as non empty finite Subset of (L ~ ) ;
A3: ex_sup_of A,L by YELLOW_0:54;
then A4: ex_inf_of A,L ~ by YELLOW_7:10;
"\/" A,L is_>=_than A by A3, YELLOW_0:def 9;
then A5: ("\/" A,L) ~ is_<=_than A by YELLOW_7:8;

now

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;

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

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

end;

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

end;