theorem :: LATWAL_2:22

for W being pcs-tol-reflexive pcs-tol-symmetric pcs-Compatible WAP-Lattice
for a, b being Element of W st a (--) b & b (--) b holds
a "/\" b (--) b "/\" b by CompDef;