for C being non empty set
for c being Element of C
for h, g being Membership_Func of C holds
( min ((h . c),(g . c)) = (min (h,g)) . c & max ((h . c),(g . c)) = (max (h,g)) . c ) by Def3, Def4;