let C be non empty set ; :: thesis: for f, g being Membership_Func of C st g c= holds
min (f,g) = f
let f, g be Membership_Func of C; :: thesis: ( g c= implies min (f,g) = f )
assume A1: g c= ; :: thesis: min (f,g) = f
A2: for x being Element of C st x in C holds
(min (f,g)) . x = f . x

proof

let x be Element of C; :: thesis: ( x in C implies (min (f,g)) . x = f . x )
f . x <= g . x by A1;
then f . x = min ((f . x),(g . x)) by XXREAL_0:def 9
.= (min (f,g)) . x by Def3 ;
hence ( x in C implies (min (f,g)) . x = f . x ) ; :: thesis: verum

end;

( C = dom (min (f,g)) & C = dom f ) by FUNCT_2:def 1;
hence min (f,g) = f by A2, PARTFUN1:5; :: thesis: verum