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 & ~ y <= c & ( 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 ) )
A3: ( c ~ = c & ~ (c ~ ) = c ~ & ~ x = x & (~ x) ~ = ~ x & ~ y = y & (~ y) ~ = ~ y ) ;
hence ( z <= x & z <= y ) by A2, 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 )
A4: ( ~ z' = z' & (~ z') ~ = ~ z' ) ;
assume ( z' <= x & z' <= y ) ; :: thesis: z' <= z
then ( ~ x <= ~ z' & ~ y <= ~ z' ) by A3, A4, Th9;
then c <= ~ z' by A2;
hence z' <= z by A4, Th9; :: thesis: verum

end;

assume A5: 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
A6: ( z <= a ~ & z <= b ~ & ( for z' being Element of (A ~ ) st z' <= a ~ & z' <= b ~ holds
z' <= z ) ) by A5;
take c = ~ z; :: thesis: ( a <= c & b <= c & ( for z' being Element of A st a <= z' & b <= z' holds
c <= z' ) )
A7: ( ~ z = z & (~ z) ~ = ~ z & a ~ = a & ~ (a ~ ) = a ~ & b ~ = b & ~ (b ~ ) = b ~ ) ;
hence ( a <= c & b <= c ) by A6, 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 ( a <= c' & b <= c' ) ; :: thesis: c <= c'
then ( c' ~ <= a ~ & c' ~ <= b ~ ) by Th9;
then c' ~ <= z by A6;
hence c <= c' by A7, Th9; :: thesis: verum