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

proof

let a1, a2, b1, b2 be Element of P; :: thesis: ( a1 "\/" a2 (--) b1 "\/" b2 & a1 "/\" a2 (--) b1 "/\" b2 )
set X = the carrier of P;
( [(a1 "\/" a2),(b1 "\/" b2)] in [: the carrier of P, the carrier of P:] & [(a1 "/\" a2),(b1 "/\" b2)] in [: the carrier of P, the carrier of P:] ) by ZFMISC_1:def 2;
then ( [(a1 "\/" a2),(b1 "\/" b2)] in nabla the carrier of P & [(a1 "/\" a2),(b1 "/\" b2)] in nabla the carrier of P ) by EQREL_1:def 1;
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