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