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 )

ex a being Element of L st

( a in A & x <= a ) ) implies x is co-prime ) :: thesis: verum

( 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

thus
( ( for A being non empty finite Subset of L st x <= sup A holds
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;

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;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)) ~

ex_inf_of A,L ~
by A3, YELLOW_7:10;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;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

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

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

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

end;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 ~ )

then
x ~ is prime
;( 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;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

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