let S, T be RelStr ; :: thesis: ( S,T are_isomorphic & S is lower-bounded implies T is lower-bounded )
given f being Function of S,T such that A1: f is isomorphic ; :: according to WAYBEL_1:def 8 :: thesis: ( not S is lower-bounded or T is lower-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 lower-bounded or T is lower-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 4 :: thesis: T is lower-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 4 :: thesis: y is_<=_than the carrier of T
y is_<=_than g .: ([#] S) by A1, A2, YELLOW_2:13;
then y is_<=_than rng g by RELSET_1:22;
hence y is_<=_than the carrier of T by A1, WAYBEL_0:66; :: thesis: verum

end;

suppose ( S is empty or T is empty ) ; :: thesis: ( not S is lower-bounded or T is lower-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 lower-bounded or T is lower-bounded ) ; :: thesis: verum

end;

end;