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