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 c9 being Element of A st a <= c9 & b <= c9 holds
c <= c9 ) ) ; :: 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 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 ~ ; :: thesis: ( 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; :: thesis: for z9 being Element of (A ~) st z9 <= x & z9 <= y holds
z9 <= z
let z9 be Element of (A ~); :: thesis: ( z9 <= x & z9 <= y implies z9 <= z )
A7: (~ z9) ~ = ~ z9 ;
assume that
A8: z9 <= x and
A9: z9 <= y ; :: thesis: 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; :: thesis: 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 ) ) ; :: 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 z9 being Element of A st a <= z9 & y <= z9 holds
z <= z9 ) )
let b be Element of A; :: thesis: 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; :: thesis: ( 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; :: thesis: for z9 being Element of A st a <= z9 & b <= z9 holds
c <= z9
let c9 be Element of A; :: thesis: ( a <= c9 & b <= c9 implies c <= c9 )
assume that
A16: a <= c9 and
A17: b <= c9 ; :: thesis: 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; :: thesis: verum