let A be non empty set ; :: thesis: for p, q being Element of holds (minfuncreal A) . p,q = (minfuncreal A) . q,p
let p, q be Element of ; :: thesis: (minfuncreal A) . p,q = (minfuncreal A) . q,p
thus (minfuncreal A) . p,q = q "/\" p by LATTICES:def 2
.= (minfuncreal A) . q,p ; :: thesis: verum