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

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