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