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 ex c being Element of st
( a <= c & b <= c & ( for c' being Element of st a <= c' & b <= c' holds
c <= c' ) ) ; :: according to LATTICE3:def 10 :: thesis: A ~ is with_infima
let x, y be Element of ; :: according to LATTICE3:def 11 :: thesis: ex z being Element of st
( z <= x & z <= y & ( for z' being Element of st z' <= x & z' <= y holds
z' <= z ) )
consider c being Element of such that
A2: ~ x <= c and
A3: ~ y <= c and
A4: for c' being Element of st ~ x <= c' & ~ y <= c' holds
c <= c' by A1;
take z = c ~ ; :: thesis: ( z <= x & z <= y & ( for z' being Element of 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 st z' <= x & z' <= y holds
z' <= z
let z' be Element of ; :: 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 ex z being Element of st
( z <= x & z <= y & ( for z' being Element of st z' <= x & z' <= y holds
z' <= z ) ) ; :: according to LATTICE3:def 11 :: thesis: A is with_suprema
let a be Element of ; :: according to LATTICE3:def 10 :: thesis: for y being Element of ex z being Element of st
( a <= z & y <= z & ( for z' being Element of st a <= z' & y <= z' holds
z <= z' ) )
let b be Element of ; :: thesis: ex z being Element of st
( a <= z & b <= z & ( for z' being Element of st a <= z' & b <= z' holds
z <= z' ) )
consider z being Element of such that
A12: z <= a ~ and
A13: z <= b ~ and
A14: for z' being Element of st z' <= a ~ & z' <= b ~ holds
z' <= z by A11;
take c = ~ z; :: thesis: ( a <= c & b <= c & ( for z' being Element of 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 st a <= z' & b <= z' holds
c <= z'
let c' be Element of ; :: 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