let p, q be Element of Nat_Lattice; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( hcflat . (q,(lcmlat . (p,q))) = q & hcflat . ((lcmlat . (q,p)),q) = q )

thus hcflat . (q,(lcmlat . (p,q))) = q by A1, Th5; :: thesis: hcflat . ((lcmlat . (q,p)),q) = q

thus hcflat . ((lcmlat . (q,p)),q) = q by A2, Th5; :: thesis: verum

set s = q "\/" p;

thus A1: hcflat . (q,(lcmlat . (q,p))) = q "/\" (q "\/" p)

.= q by NEWTON:54 ; :: thesis: ( 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 ; :: thesis: ( hcflat . (q,(lcmlat . (p,q))) = q & hcflat . ((lcmlat . (q,p)),q) = q )

thus hcflat . (q,(lcmlat . (p,q))) = q by A1, Th5; :: thesis: hcflat . ((lcmlat . (q,p)),q) = q

thus hcflat . ((lcmlat . (q,p)),q) = q by A2, Th5; :: thesis: verum