let p, q 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:53 ; :: 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:53 ; :: thesis: ( lcmlat . (q,(hcflat . (p,q))) = q & lcmlat . ((hcflat . (q,p)),q) = q )
thus lcmlat . (q,(hcflat . (p,q))) = q by A1, Th6; :: thesis: lcmlat . ((hcflat . (q,p)),q) = q
thus lcmlat . ((hcflat . (q,p)),q) = q by A2, Th6; :: thesis: verum