let C be non empty set ; :: thesis: for f, g being Membership_Func of C holds min (f,g) = ((C,f) @) "/\" ((C,g) @)
let f, g be Membership_Func of C; :: thesis: min (f,g) = ((C,f) @) "/\" ((C,g) @)
set fg = ((C,f) @) "/\" ((C,g) @);
set R = RealPoset [.0,1.];
set J = C --> (RealPoset [.0,1.]);
A1: (RealPoset [.0,1.]) |^ C = product (C --> (RealPoset [.0,1.])) by YELLOW_1:def 5;

now :: thesis: for c being Element of C holds (@ (((C,f) @) "/\" ((C,g) @))) . c = min ((f . c),(g . c))

let c be Element of C; :: thesis: (@ (((C,f) @) "/\" ((C,g) @))) . c = min ((f . c),(g . c))
( ( for c being Element of C holds (C --> (RealPoset [.0,1.])) . c is Semilattice ) & (C --> (RealPoset [.0,1.])) . c = RealPoset [.0,1.] ) ;
hence (@ (((C,f) @) "/\" ((C,g) @))) . c = (((C,f) @) . c) "/\" (((C,g) @) . c) by A1, Th11
.= min ((f . c),(g . c)) ;
:: thesis: verum

end;

hence min (f,g) = ((C,f) @) "/\" ((C,g) @) by FUZZY_1:def 3; :: thesis: verum