let S, T be non empty reflexive antisymmetric up-complete RelStr ; 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:]; ( x << y implies ( x `1 << y `1 & x `2 << y `2 ) )
assume A1:
x << y
; ( 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; verum