let S, T be non empty RelStr ; ( 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
; WAYBEL_1:def 8 ( 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 ) )
; LATTICE3:def 10 T is with_suprema
let x, y be Element of T; LATTICE3:def 10 ex b1 being Element of the carrier of T st
( x <= b1 & y <= b1 & ( for b2 being Element of the carrier of T holds
( not x <= b2 or not y <= b2 or b1 <= b2 ) ) )
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
; ( x <= f . c & y <= f . c & ( for b1 being Element of the carrier of T holds
( not x <= b1 or not y <= b1 or f . c <= b1 ) ) )
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; for b1 being Element of the carrier of T holds
( not x <= b1 or not y <= b1 or f . c <= b1 )
let z9 be Element of T; ( not x <= z9 or not y <= z9 or f . c <= z9 )
assume
( x <= z9 & y <= z9 )
; 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; verum