let R, S be RelStr ; :: thesis: for a, b being Element of (R [*] S) st the carrier of R /\ the carrier of S is upper Subset of R & a <= b & a in the carrier of S holds
b in the carrier of S
let a, b be Element of (R [*] S); :: thesis: ( the carrier of R /\ the carrier of S is upper Subset of R & a <= b & a in the carrier of S implies b in the carrier of S )
assume that
A1: the carrier of R /\ the carrier of S is upper Subset of R and
A2: a <= b and
A3: a in the carrier of S ; :: thesis: b in the carrier of S
[a,b] in the InternalRel of (R [*] S) by A2, ORDERS_2:def 5;
hence b in the carrier of S by A1, A3, Th17; :: thesis: verum