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 consider a, b being set such that
A2: ( a in the carrier of S1 & b in the carrier of S2 & x = [a,b] ) by ZFMISC_1:def 2;
consider c, d being set such that
A3: ( c in the carrier of S1 & d in the carrier of S2 & y = [c,d] ) by A1, ZFMISC_1:def 2;
( x = [(x `1 ),(x `2 )] & y = [(y `1 ),(y `2 )] ) by A2, A3, MCART_1:8;
hence ( x <= y iff ( x `1 <= y `1 & x `2 <= y `2 ) ) by Th11; :: thesis: verum