let p, q, r be Element of Real_Lattice; :: thesis: ( 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) )
set s = q "/\" r;
thus A1: minreal . (p,(minreal . (q,r))) = (q "/\" r) "/\" p by LATTICES:def 2
.= minreal . ((minreal . (q,r)),p) ; :: thesis: ( 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) )
thus minreal . (p,(minreal . (q,r))) = p "/\" (q "/\" r)
.= (p "/\" q) "/\" r by XXREAL_0:33
.= minreal . ((minreal . (p,q)),r) ; :: thesis: ( 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) )
thus minreal . (p,(minreal . (q,r))) = p "/\" (q "/\" r)
.= (q "/\" p) "/\" r by XXREAL_0:33
.= minreal . ((minreal . (q,p)),r) ; :: thesis: ( 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) )
thus A2: minreal . (p,(minreal . (q,r))) = p "/\" (q "/\" r)
.= (r "/\" p) "/\" q by XXREAL_0:33
.= minreal . ((minreal . (r,p)),q) ; :: thesis: ( minreal . (p,(minreal . (q,r))) = minreal . ((minreal . (r,q)),p) & minreal . (p,(minreal . (q,r))) = minreal . ((minreal . (p,r)),q) )
thus minreal . (p,(minreal . (q,r))) = minreal . ((minreal . (r,q)),p) by A1, Th2; :: thesis: minreal . (p,(minreal . (q,r))) = minreal . ((minreal . (p,r)),q)
thus minreal . (p,(minreal . (q,r))) = minreal . ((minreal . (p,r)),q) by A2, Th2; :: thesis: verum