let W be pcs-tol-reflexive pcs-tol-symmetric pcs-Compatible WAP-Lattice; :: thesis: for a, b being Element of W st a (--) b & b (--) b holds
a "/\" b (--) b
let a, b be Element of W; :: thesis: ( a (--) b & b (--) b implies a "/\" b (--) b )
assume ( a (--) b & b (--) b ) ; :: thesis: a "/\" b (--) b
then a "/\" b (--) b "/\" b by CompDef;
hence a "/\" b (--) b by LemmaId; :: thesis: verum