let S, T be non empty reflexive antisymmetric up-complete RelStr ; :: thesis: for x, y being Element of [:S,T:] st x << y holds
( x `1 << y `1 & x `2 << y `2 )
let x, y be Element of [:S,T:]; :: thesis: ( x << y implies ( x `1 << y `1 & x `2 << y `2 ) )
assume A1: x << y ; :: thesis: ( x `1 << y `1 & x `2 << y `2 )
the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def 2;
then ( x = [(x `1),(x `2)] & y = [(y `1),(y `2)] ) by MCART_1:21;
hence ( x `1 << y `1 & x `2 << y `2 ) by A1, Th18; :: thesis: verum