let P be non empty pcs-Str ; :: thesis: ( the ToleranceRel of P = id the carrier of P implies P is pcs-Compatible )
assume A1: the ToleranceRel of P = id the carrier of P ; :: thesis: P is pcs-Compatible
for a1, a2, b1, b2 being Element of P st a1 (--) b1 & a2 (--) b2 holds
( a1 "\/" a2 (--) b1 "\/" b2 & a1 "/\" a2 (--) b1 "/\" b2 )

proof

let a1, a2, b1, b2 be Element of P; :: thesis: ( a1 (--) b1 & a2 (--) b2 implies ( a1 "\/" a2 (--) b1 "\/" b2 & a1 "/\" a2 (--) b1 "/\" b2 ) )
assume ( a1 (--) b1 & a2 (--) b2 ) ; :: thesis: ( a1 "\/" a2 (--) b1 "\/" b2 & a1 "/\" a2 (--) b1 "/\" b2 )
then ( [a1,b1] in the ToleranceRel of P & [a2,b2] in the ToleranceRel of P ) by PCS_0:def 7;
then ( a1 = b1 & a2 = b2 ) by A1, RELAT_1:def 10;
then ( [(a1 "\/" a2),(b1 "\/" b2)] in id the carrier of P & [(a1 "/\" a2),(b1 "/\" b2)] in id the carrier of P ) by RELAT_1:def 10;
hence ( a1 "\/" a2 (--) b1 "\/" b2 & a1 "/\" a2 (--) b1 "/\" b2 ) by A1, PCS_0:def 7; :: thesis: verum

end;

hence P is pcs-Compatible ; :: thesis: verum