theorem :: LATWAL_2:21

for W being pcs-tol-reflexive pcs-tol-symmetric pcs-Compatible WAP-Lattice
for x, y being Element of W st x (--) y holds
y (--) x ;