let W be pcs-tol-reflexive pcs-tol-symmetric pcs-Compatible WAP-Lattice; :: thesis: for x being Element of W holds x (--) x
let x be Element of W; :: thesis: x (--) x
A1: the ToleranceRel of W is_reflexive_in the carrier of W by PCS_0:def 9;
[x,x] in the ToleranceRel of W by A1, RELAT_2:def 1;
hence x (--) x by PCS_0:def 7; :: thesis: verum