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, Th9; :: thesis: minreal . p,(minreal . q,r) = minreal . (minreal . p,r),q
thus minreal . p,(minreal . q,r) = minreal . (minreal . p,r),q by A2, Th9; :: thesis: verum