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 LemmaId2; :: thesis: verum