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