let R be non empty with_suprema Poset; :: thesis: for l being Element of R holds
( l is co-prime iff for x, y being Element of R holds
( not l <= x "\/" y or l <= x or l <= y ) )
let l be Element of R; :: thesis: ( l is co-prime iff for x, y being Element of R holds
( not l <= x "\/" y or l <= x or l <= y ) )
hereby :: thesis: ( ( for x, y being Element of R holds
( not l <= x "\/" y or l <= x or l <= y ) ) implies l is co-prime )
assume l is co-prime ; :: thesis: for x, y being Element of R holds
( not l <= x "\/" y or l <= x or l <= y )
then A1: l ~ is prime ;
let x, y be Element of R; :: thesis: ( not l <= x "\/" y or l <= x or l <= y )
assume l <= x "\/" y ; :: thesis: ( l <= x or l <= y )
then A2: (x "\/" y) ~ <= l ~ by LATTICE3:9;
(x "\/" y) ~ = x "\/" y by LATTICE3:def 6
.= (x ~) "/\" (y ~) by YELLOW_7:23 ;
then ( x ~ <= l ~ or y ~ <= l ~ ) by A1, A2;
hence ( l <= x or l <= y ) by LATTICE3:9; :: thesis: verum
end;
assume A3: for x, y being Element of R holds
( not l <= x "\/" y or l <= x or l <= y ) ; :: thesis: l is co-prime
let x, y be Element of (R ~); :: according to WAYBEL_6:def 6,WAYBEL_6:def 8 :: thesis: ( not x "/\" y <= l ~ or x <= l ~ or y <= l ~ )
A4: ~ (x "/\" y) = x "/\" y by LATTICE3:def 7
.= (~ x) "\/" (~ y) by YELLOW_7:24 ;
assume x "/\" y <= l ~ ; :: thesis: ( x <= l ~ or y <= l ~ )
then l <= (~ x) "\/" (~ y) by A4, YELLOW_7:2;
then ( l <= ~ x or l <= ~ y ) by A3;
hence ( x <= l ~ or y <= l ~ ) by YELLOW_7:2; :: thesis: verum