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 c9 being Element of S st a <= c9 & b <= c9 holds
c <= c9 ) ) ; :: 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 c9 being Element of S st (f /") . x <= c9 & (f /") . y <= c9 holds
c <= c9 by A2;
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₁ ) ) )
A5: ex g being Function of T,S st
( g = f " & g is monotone ) by A1, WAYBEL_0:def 38;
A6: rng f = the carrier of T by A1, WAYBEL_0:66;
A7: f /" = f " by A1, TOPS_2:def 4;
( f . ((f /") . x) <= f . c & f . ((f /") . y) <= f . c ) by A1, A3, WAYBEL_0:66;
hence ( x <= f . c & y <= f . c ) by A1, A6, A7, FUNCT_1:35; :: thesis: for b₁ being Element of the carrier of T holds
( not x <= b₁ or not y <= b₁ or f . c <= b₁ )
let z9 be Element of T; :: thesis: ( not x <= z9 or not y <= z9 or f . c <= z9 )
assume ( x <= z9 & y <= z9 ) ; :: thesis: f . c <= z9
then ( (f /") . x <= (f /") . z9 & (f /") . y <= (f /") . z9 ) by A7, A5, WAYBEL_1:def 2;
then c <= (f /") . z9 by A4;
then f . c <= f . ((f /") . z9) by A1, WAYBEL_0:66;
hence f . c <= z9 by A1, A6, A7, FUNCT_1:35; :: thesis: verum