let S, T be non empty RelStr ; :: thesis: ( S,T are_isomorphic & S is with_suprema implies T is with_suprema )
given f being Function of S,T such that A1: f is isomorphic ; :: according to WAYBEL_1:def 8 :: thesis: ( not S is with_suprema or T is with_suprema )
assume A2: for a, b being Element of S ex c being Element of S st
( a <= c & b <= c & ( for c' being Element of S st a <= c' & b <= c' holds
c <= c' ) ) ; :: according to LATTICE3:def 10 :: thesis: T is with_suprema
let x, y be Element of T; :: according to LATTICE3:def 10 :: thesis: ex b₁ being Element of the carrier of T st
( x <= b₁ & y <= b₁ & ( for b₂ being Element of the carrier of T holds
( not x <= b₂ or not y <= b₂ or b₁ <= b₂ ) ) )
consider c being Element of S such that
A3: ( (f /" ) . x <= c & (f /" ) . y <= c ) and
A4: for c' being Element of S st (f /" ) . x <= c' & (f /" ) . y <= c' holds
c <= c' by A2;
A5: ( f is one-to-one & rng f = the carrier of T ) by A1, WAYBEL_0:66;
then A6: f /" = f " by TOPS_2:def 4;
take f . c ; :: thesis: ( x <= f . c & y <= f . c & ( for b₁ being Element of the carrier of T holds
( not x <= b₁ or not y <= b₁ or f . c <= b₁ ) ) )
( f . ((f /" ) . x) <= f . c & f . ((f /" ) . y) <= f . c ) by A1, A3, WAYBEL_0:66;
hence ( x <= f . c & y <= f . c ) by A5, A6, FUNCT_1:57; :: thesis: for b₁ being Element of the carrier of T holds
( not x <= b₁ or not y <= b₁ or f . c <= b₁ )
let z' be Element of T; :: thesis: ( not x <= z' or not y <= z' or f . c <= z' )
assume A7: ( x <= z' & y <= z' ) ; :: thesis: f . c <= z'
ex g being Function of T,S st
( g = f " & g is monotone ) by A1, WAYBEL_0:def 38;
then ( (f /" ) . x <= (f /" ) . z' & (f /" ) . y <= (f /" ) . z' ) by A6, A7, WAYBEL_1:def 2;
then c <= (f /" ) . z' by A4;
then f . c <= f . ((f /" ) . z') by A1, WAYBEL_0:66;
hence f . c <= z' by A5, A6, FUNCT_1:57; :: thesis: verum