let P1, P2 be RelStr ; :: thesis: ( RelStr(# the carrier of P1, the InternalRel of P1 #) = RelStr(# the carrier of P2, the InternalRel of P2 #) implies ( ( P1 is lower-bounded implies P2 is lower-bounded ) & ( P1 is upper-bounded implies P2 is upper-bounded ) ) )
assume A1: RelStr(# the carrier of P1, the InternalRel of P1 #) = RelStr(# the carrier of P2, the InternalRel of P2 #) ; :: thesis: ( ( P1 is lower-bounded implies P2 is lower-bounded ) & ( P1 is upper-bounded implies P2 is upper-bounded ) )
thus ( P1 is lower-bounded implies P2 is lower-bounded ) :: thesis: ( P1 is upper-bounded implies P2 is upper-bounded )

proof

given x being Element of P1 such that A2: x is_<=_than the carrier of P1 ; :: according to YELLOW_0:def 4 :: thesis: P2 is lower-bounded
reconsider y = x as Element of P2 by A1;
take y ; :: according to YELLOW_0:def 4 :: thesis: y is_<=_than the carrier of P2
thus y is_<=_than the carrier of P2 by A1, A2, Th2; :: thesis: verum

end;

given x being Element of P1 such that A3: x is_>=_than the carrier of P1 ; :: according to YELLOW_0:def 5 :: thesis: P2 is upper-bounded
reconsider y = x as Element of P2 by A1;
take y ; :: according to YELLOW_0:def 5 :: thesis: y is_>=_than the carrier of P2
thus y is_>=_than the carrier of P2 by A1, A3, Th2; :: thesis: verum