let S1, S2 be non empty TolStr ; :: thesis: for a, c being Element of S1
for b, d being Element of S2 holds
( [^a,b^] (--) [^c,d^] iff ( a (--) c or b (--) d ) )
let a, c be Element of S1; :: thesis: for b, d being Element of S2 holds
( [^a,b^] (--) [^c,d^] iff ( a (--) c or b (--) d ) )
let b, d be Element of S2; :: thesis: ( [^a,b^] (--) [^c,d^] iff ( a (--) c or b (--) d ) )
set I1 = the ToleranceRel of S1;
set I2 = the ToleranceRel of S2;
set x = [[a,b],[c,d]];
A1: ([[a,b],[c,d]] `1 ) `1 = a by Lm2;
A2: ([[a,b],[c,d]] `1 ) `2 = b by Lm2;
A3: ([[a,b],[c,d]] `2 ) `1 = c by Lm2;
A4: ([[a,b],[c,d]] `2 ) `2 = d by Lm2;
thus ( not [^a,b^] (--) [^c,d^] or a (--) c or b (--) d ) :: thesis: ( ( a (--) c or b (--) d ) implies [^a,b^] (--) [^c,d^] )

proof

assume [^a,b^] (--) [^c,d^] ; :: thesis: ( a (--) c or b (--) d )
then [[a,b],[c,d]] in the ToleranceRel of [^S1,S2^] by Def7;
then ( [a,c] in the ToleranceRel of S1 or [b,d] in the ToleranceRel of S2 ) by Def3;
hence ( a (--) c or b (--) d ) by Def7; :: thesis: verum

end;

assume ( a (--) c or b (--) d ) ; :: thesis: [^a,b^] (--) [^c,d^]
then ( [(([[a,b],[c,d]] `1 ) `1 ),(([[a,b],[c,d]] `2 ) `1 )] in the ToleranceRel of S1 or [(([[a,b],[c,d]] `1 ) `2 ),(([[a,b],[c,d]] `2 ) `2 )] in the ToleranceRel of S2 ) by A1, A2, A3, A4, Def7;
hence [[a,b],[c,d]] in the ToleranceRel of [^S1,S2^] by A1, A2, A3, A4, Def3; :: according to PCS_0:def 7 :: thesis: verum