let A be RelStr ; ( A is with_suprema iff A ~ is with_infima )
thus
( A is with_suprema implies A ~ is with_infima )
( A ~ is with_infima implies A is with_suprema )proof
assume A1:
for
a,
b being
Element of
A ex
c being
Element of
A st
(
a <= c &
b <= c & ( for
c9 being
Element of
A st
a <= c9 &
b <= c9 holds
c <= c9 ) )
;
LATTICE3:def 10 A ~ is with_infima
let x,
y be
Element of
(A ~);
LATTICE3:def 11 ex z being Element of (A ~) st
( z <= x & z <= y & ( for z9 being Element of (A ~) st z9 <= x & z9 <= y holds
z9 <= z ) )
consider c being
Element of
A such that A2:
~ x <= c
and A3:
~ y <= c
and A4:
for
c9 being
Element of
A st
~ x <= c9 &
~ y <= c9 holds
c <= c9
by A1;
take z =
c ~ ;
( z <= x & z <= y & ( for z9 being Element of (A ~) st z9 <= x & z9 <= y holds
z9 <= z ) )
A5:
(~ x) ~ = ~ x
;
A6:
(~ y) ~ = ~ y
;
hence
(
z <= x &
z <= y )
by A2, A3, A5, Th9;
for z9 being Element of (A ~) st z9 <= x & z9 <= y holds
z9 <= z
let z9 be
Element of
(A ~);
( z9 <= x & z9 <= y implies z9 <= z )
A7:
(~ z9) ~ = ~ z9
;
assume that A8:
z9 <= x
and A9:
z9 <= y
;
z9 <= z
A10:
~ x <= ~ z9
by A5, A7, A8, Th9;
~ y <= ~ z9
by A6, A7, A9, Th9;
then
c <= ~ z9
by A4, A10;
hence
z9 <= z
by A7, Th9;
verum
end;
assume A11:
for x, y being Element of (A ~) ex z being Element of (A ~) st
( z <= x & z <= y & ( for z9 being Element of (A ~) st z9 <= x & z9 <= y holds
z9 <= z ) )
; LATTICE3:def 11 A is with_suprema
let a be Element of A; LATTICE3:def 10 for y being Element of A ex z being Element of A st
( a <= z & y <= z & ( for z9 being Element of A st a <= z9 & y <= z9 holds
z <= z9 ) )
let b be Element of A; ex z being Element of A st
( a <= z & b <= z & ( for z9 being Element of A st a <= z9 & b <= z9 holds
z <= z9 ) )
consider z being Element of (A ~) such that
A12:
z <= a ~
and
A13:
z <= b ~
and
A14:
for z9 being Element of (A ~) st z9 <= a ~ & z9 <= b ~ holds
z9 <= z
by A11;
take c = ~ z; ( a <= c & b <= c & ( for z9 being Element of A st a <= z9 & b <= z9 holds
c <= z9 ) )
A15:
(~ z) ~ = ~ z
;
hence
( a <= c & b <= c )
by A12, A13, Th9; for z9 being Element of A st a <= z9 & b <= z9 holds
c <= z9
let c9 be Element of A; ( a <= c9 & b <= c9 implies c <= c9 )
assume that
A16:
a <= c9
and
A17:
b <= c9
; c <= c9
A18:
c9 ~ <= a ~
by A16, Th9;
c9 ~ <= b ~
by A17, Th9;
then
c9 ~ <= z
by A14, A18;
hence
c <= c9
by A15, Th9; verum