let S, T be non empty up-complete Poset; :: thesis: for x, y being Element of [:S,T:] holds
( x << y iff ( x `1 << y `1 & x `2 << y `2 ) )
let x, y be Element of [:S,T:]; :: thesis: ( x << y iff ( 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 << y iff ( x `1 << y `1 & x `2 << y `2 ) ) by Th19; :: thesis: verum