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 & ([[a,b],[c,d]] `1 ) `2 = b & ([[a,b],[c,d]] `2 ) `1 = c & ([[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, Def7;
hence [[a,b],[c,d]] in the ToleranceRel of [^S1,S2^] by A1, Def3; :: according to PCS_0:def 7 :: thesis: verum