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