let S1, S2 be non empty RelStr ; :: thesis: for x, y being Element of [:S1,S2:] holds
( x <= y iff ( x `1 <= y `1 & x `2 <= y `2 ) )
let x, y be Element of [:S1,S2:]; :: thesis: ( x <= y iff ( x `1 <= y `1 & x `2 <= y `2 ) )
A1: the carrier of [:S1,S2:] = [: the carrier of S1, the carrier of S2:] by Def2;
then ex c, d being object st
( c in the carrier of S1 & d in the carrier of S2 & y = [c,d] ) by ZFMISC_1:def 2;
then A2: y = [(y `1),(y `2)] ;
ex a, b being object st
( a in the carrier of S1 & b in the carrier of S2 & x = [a,b] ) by A1, ZFMISC_1:def 2;
then x = [(x `1),(x `2)] ;
hence ( x <= y iff ( x `1 <= y `1 & x `2 <= y `2 ) ) by A2, Th11; :: thesis: verum