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: ( C = dom (min f,g) & C = dom f ) by FUNCT_2:def 1;
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, Def3;
then f . x = min (f . x),(g . x) by XXREAL_0:def 9
.= (min f,g) . x by Def4 ;
hence ( x in C implies (min f,g) . x = f . x ) ; :: thesis: verum

end;

hence min f,g = f by A2, PARTFUN1:34; :: thesis: verum