let C be non empty set ; for f, g being Membership_Func of C holds min (f,g) = ((C,f) @) "/\" ((C,g) @)
let f, g be Membership_Func of C; 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 for c being Element of C holds (@ (((C,f) @) "/\" ((C,g) @))) . c = min ((f . c),(g . c))let c be
Element of
C;
(@ (((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))
;
verum end;
hence
min (f,g) = ((C,f) @) "/\" ((C,g) @)
by FUZZY_1:def 3; verum