let q, p be Element of Nat_Lattice ; :: thesis: ( lcmlat . q,(hcflat . q,p) = q & lcmlat . (hcflat . p,q),q = q & lcmlat . q,(hcflat . p,q) = q & lcmlat . (hcflat . q,p),q = q )
set r = p "/\" q;
thus A1: lcmlat . q,(hcflat . q,p) = lcmlat . q,(q "/\" p)
.= (p "/\" q) "\/" q by LATTICES:def 1
.= q by NEWTON:66 ; :: thesis: ( lcmlat . (hcflat . p,q),q = q & lcmlat . q,(hcflat . p,q) = q & lcmlat . (hcflat . q,p),q = q )
thus A2: lcmlat . (hcflat . p,q),q = (p "/\" q) "\/" q
.= q by NEWTON:66 ; :: thesis: ( lcmlat . q,(hcflat . p,q) = q & lcmlat . (hcflat . q,p),q = q )
thus lcmlat . q,(hcflat . p,q) = q by A1, Th62; :: thesis: lcmlat . (hcflat . q,p),q = q
thus lcmlat . (hcflat . q,p),q = q by A2, Th62; :: thesis: verum