let A be non empty set ; :: thesis: for p, q, r being Element of (RealFunc_Lattice A) holds
( (minfuncreal A) . p,((minfuncreal A) . q,r) = (minfuncreal A) . ((minfuncreal A) . q,r),p & (minfuncreal A) . p,((minfuncreal A) . q,r) = (minfuncreal A) . ((minfuncreal A) . p,q),r & (minfuncreal A) . p,((minfuncreal A) . q,r) = (minfuncreal A) . ((minfuncreal A) . q,p),r & (minfuncreal A) . p,((minfuncreal A) . q,r) = (minfuncreal A) . ((minfuncreal A) . r,p),q & (minfuncreal A) . p,((minfuncreal A) . q,r) = (minfuncreal A) . ((minfuncreal A) . r,q),p & (minfuncreal A) . p,((minfuncreal A) . q,r) = (minfuncreal A) . ((minfuncreal A) . p,r),q )
let p, q, r be Element of (RealFunc_Lattice A); :: thesis: ( (minfuncreal A) . p,((minfuncreal A) . q,r) = (minfuncreal A) . ((minfuncreal A) . q,r),p & (minfuncreal A) . p,((minfuncreal A) . q,r) = (minfuncreal A) . ((minfuncreal A) . p,q),r & (minfuncreal A) . p,((minfuncreal A) . q,r) = (minfuncreal A) . ((minfuncreal A) . q,p),r & (minfuncreal A) . p,((minfuncreal A) . q,r) = (minfuncreal A) . ((minfuncreal A) . r,p),q & (minfuncreal A) . p,((minfuncreal A) . q,r) = (minfuncreal A) . ((minfuncreal A) . r,q),p & (minfuncreal A) . p,((minfuncreal A) . q,r) = (minfuncreal A) . ((minfuncreal A) . p,r),q )
set s = q "/\" r;
thus A1: (minfuncreal A) . p,((minfuncreal A) . q,r) = (q "/\" r) "/\" p by LATTICES:def 2
.= (minfuncreal A) . ((minfuncreal A) . q,r),p ; :: thesis: ( (minfuncreal A) . p,((minfuncreal A) . q,r) = (minfuncreal A) . ((minfuncreal A) . p,q),r & (minfuncreal A) . p,((minfuncreal A) . q,r) = (minfuncreal A) . ((minfuncreal A) . q,p),r & (minfuncreal A) . p,((minfuncreal A) . q,r) = (minfuncreal A) . ((minfuncreal A) . r,p),q & (minfuncreal A) . p,((minfuncreal A) . q,r) = (minfuncreal A) . ((minfuncreal A) . r,q),p & (minfuncreal A) . p,((minfuncreal A) . q,r) = (minfuncreal A) . ((minfuncreal A) . p,r),q )
thus (minfuncreal A) . p,((minfuncreal A) . q,r) = (minfuncreal A) . ((minfuncreal A) . p,q),r by Th23; :: thesis: ( (minfuncreal A) . p,((minfuncreal A) . q,r) = (minfuncreal A) . ((minfuncreal A) . q,p),r & (minfuncreal A) . p,((minfuncreal A) . q,r) = (minfuncreal A) . ((minfuncreal A) . r,p),q & (minfuncreal A) . p,((minfuncreal A) . q,r) = (minfuncreal A) . ((minfuncreal A) . r,q),p & (minfuncreal A) . p,((minfuncreal A) . q,r) = (minfuncreal A) . ((minfuncreal A) . p,r),q )
thus (minfuncreal A) . p,((minfuncreal A) . q,r) = p "/\" (q "/\" r)
.= (q "/\" p) "/\" r by Lm10
.= (minfuncreal A) . ((minfuncreal A) . q,p),r ; :: thesis: ( (minfuncreal A) . p,((minfuncreal A) . q,r) = (minfuncreal A) . ((minfuncreal A) . r,p),q & (minfuncreal A) . p,((minfuncreal A) . q,r) = (minfuncreal A) . ((minfuncreal A) . r,q),p & (minfuncreal A) . p,((minfuncreal A) . q,r) = (minfuncreal A) . ((minfuncreal A) . p,r),q )
thus A2: (minfuncreal A) . p,((minfuncreal A) . q,r) = p "/\" (q "/\" r)
.= (r "/\" p) "/\" q by Lm10
.= (minfuncreal A) . ((minfuncreal A) . r,p),q ; :: thesis: ( (minfuncreal A) . p,((minfuncreal A) . q,r) = (minfuncreal A) . ((minfuncreal A) . r,q),p & (minfuncreal A) . p,((minfuncreal A) . q,r) = (minfuncreal A) . ((minfuncreal A) . p,r),q )
thus (minfuncreal A) . p,((minfuncreal A) . q,r) = (minfuncreal A) . ((minfuncreal A) . r,q),p by A1, Th41; :: thesis: (minfuncreal A) . p,((minfuncreal A) . q,r) = (minfuncreal A) . ((minfuncreal A) . p,r),q
thus (minfuncreal A) . p,((minfuncreal A) . q,r) = (minfuncreal A) . ((minfuncreal A) . p,r),q by A2, Th41; :: thesis: verum