theorem Th4: :: REAL_LAT:4

for p, q, r being Element of Real_Lattice holds
( minreal . (p,(minreal . (q,r))) = minreal . ((minreal . (q,r)),p) & minreal . (p,(minreal . (q,r))) = minreal . ((minreal . (p,q)),r) & minreal . (p,(minreal . (q,r))) = minreal . ((minreal . (q,p)),r) & minreal . (p,(minreal . (q,r))) = minreal . ((minreal . (r,p)),q) & minreal . (p,(minreal . (q,r))) = minreal . ((minreal . (r,q)),p) & minreal . (p,(minreal . (q,r))) = minreal . ((minreal . (p,r)),q) )