let L be sup-Semilattice; 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; ( 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 ) )
( ( 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
;
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;
( 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
;
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;
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
;
( ~ a in A & x <= ~ a )
thus
(
~ a in A &
x <= ~ a )
by A6, YELLOW_7:2;
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 )
verum