let f, g be Fuzzy_Negation; :: thesis: for ff, gg being Membership_Func of [.0,1.] st f = ff & g = gg holds
min (f,g) = min (ff,gg)
let ff, gg be Membership_Func of [.0,1.]; :: thesis: ( f = ff & g = gg implies min (f,g) = min (ff,gg) )
assume A1: ( f = ff & g = gg ) ; :: thesis: min (f,g) = min (ff,gg)
consider f1, g1 being Function of [.0,1.],REAL such that
A2: ( f1 = f & g1 = g & min (f,g) = min (f1,g1) ) by MinFuz;
reconsider ff1 = f1, gg1 = g1 as Membership_Func of [.0,1.] by A2;
for c being Element of [.0,1.] holds (min (ff1,gg1)) . c = min ((ff1 . c),(gg1 . c)) by FUZZY_1:def 3;
hence min (f,g) = min (ff,gg) by A1, A2, COUSIN2:def 1; :: thesis: verum