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:23;
hence ( x `1 << y `1 & x `2 << y `2 ) by A1, Th18; :: thesis: verum