let p, q be Element of Nat_Lattice; ( hcflat . (q,(lcmlat . (q,p))) = q & hcflat . ((lcmlat . (p,q)),q) = q & hcflat . (q,(lcmlat . (p,q))) = q & hcflat . ((lcmlat . (q,p)),q) = q )
set s = q "\/" p;
thus A1: hcflat . (q,(lcmlat . (q,p))) =
q "/\" (q "\/" p)
.=
q
by NEWTON:54
; ( hcflat . ((lcmlat . (p,q)),q) = q & hcflat . (q,(lcmlat . (p,q))) = q & hcflat . ((lcmlat . (q,p)),q) = q )
thus A2: hcflat . ((lcmlat . (p,q)),q) =
hcflat . ((p "\/" q),q)
.=
q "/\" (q "\/" p)
by LATTICES:def 2
.=
q
by NEWTON:54
; ( hcflat . (q,(lcmlat . (p,q))) = q & hcflat . ((lcmlat . (q,p)),q) = q )
thus
hcflat . (q,(lcmlat . (p,q))) = q
by A1, Th5; hcflat . ((lcmlat . (q,p)),q) = q
thus
hcflat . ((lcmlat . (q,p)),q) = q
by A2, Th5; verum