let S1, S2 be non empty TolStr ; :: thesis: for x, y being Element of [^S1,S2^] holds
( x (--) y iff ( x ^`1 (--) y ^`1 or x ^`2 (--) y ^`2 ) )
let x, y be Element of [^S1,S2^]; :: thesis: ( x (--) y iff ( x ^`1 (--) y ^`1 or x ^`2 (--) y ^`2 ) )
A1: ex a, b being object st
( a in the carrier of S1 & b in the carrier of S2 & x = [a,b] ) by ZFMISC_1:def 2;
A2: 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;
A3: x = [(x ^`1),(x ^`2)] by A1;
y = [(y ^`1),(y ^`2)] by A2;
hence ( x (--) y iff ( x ^`1 (--) y ^`1 or x ^`2 (--) y ^`2 ) ) by A3, Th6; :: thesis: verum