let S, T be RelStr ; :: thesis: ( S,T are_isomorphic & S is upper-bounded implies T is upper-bounded )
given f being Function of S,T such that A1: f is isomorphic ; :: according to WAYBEL_1:def 8 :: thesis: ( not S is upper-bounded or T is upper-bounded )
per cases ( ( not S is empty & not T is empty ) or S is empty or T is empty ) ;
suppose ( not S is empty & not T is empty ) ; :: thesis: ( not S is upper-bounded or T is upper-bounded )
then reconsider s = S, t = T as non empty RelStr ;
given X being Element of S such that A2: X is_>=_than the carrier of S ; :: according to YELLOW_0:def 5 :: thesis: T is upper-bounded
reconsider x = X as Element of s ;
reconsider g = f as Function of s,t ;
reconsider y = g . x as Element of T ;
take y ; :: according to YELLOW_0:def 5 :: thesis: the carrier of T is_<=_than y
y is_>=_than g .: ([#] S) by A1, A2, YELLOW_2:14;
then y is_>=_than rng g by RELSET_1:22;
hence the carrier of T is_<=_than y by A1, WAYBEL_0:66; :: thesis: verum
end;
suppose ( S is empty or T is empty ) ; :: thesis: ( not S is upper-bounded or T is upper-bounded )
then T is empty by A1, WAYBEL_0:def 38;
then reconsider T = T as bounded RelStr ;
T is lower-bounded ;
hence ( not S is upper-bounded or T is upper-bounded ) ; :: thesis: verum
end;
end;