reconsider f = N1, g = N2 as Function of [.0,1.],REAL by LemmaFunc;
set EX = min (f,g);
A1: rng (min (f,g)) c= (rng f) \/ (rng g) by LemmaMinRng;
( rng f c= [.0,1.] & rng g c= [.0,1.] ) by RELAT_1:def 19;
then (rng f) \/ (rng g) c= [.0,1.] by XBOOLE_1:8;
then rng (min (f,g)) c= [.0,1.] by A1, XBOOLE_1:1;
then reconsider EX = min (f,g) as UnOp of [.0,1.] by FUNCT_2:6;
B0: ( 0 in [.0,1.] & 1 in [.0,1.] ) by XXREAL_1:1;
B1: EX . 0 = min ((f . 0),(g . 0)) by B0, COUSIN2:def 1
.= min (1,(N2 . 0)) by FUZIMPL3:def 4
.= min (1,1) by FUZIMPL3:def 4
.= 1 ;
EX . 1 = min ((f . 1),(g . 1)) by B0, COUSIN2:def 1
.= min (0,(N2 . 1)) by FUZIMPL3:def 4
.= min (0,0) by FUZIMPL3:def 4
.= 0 ;
then C1: EX is satisfying_(N1) by B1, FUZIMPL3:def 4;
for a, b being Element of [.0,1.] st a <= b holds
EX . a >= EX . b

proof

let a, b be Element of [.0,1.]; :: thesis: ( a <= b implies EX . a >= EX . b )
assume a <= b ; :: thesis: EX . a >= EX . b
then ( f . a >= f . b & g . a >= g . b ) by FUZIMPL3:7;
then min ((f . a),(g . a)) >= min ((f . b),(g . b)) by XXREAL_0:18;
then (min (f,g)) . a >= min ((f . b),(g . b)) by COUSIN2:def 1;
hence EX . a >= EX . b by COUSIN2:def 1; :: thesis: verum

end;

then reconsider EX = EX as Fuzzy_Negation by C1, FUZIMPL3:def 5, FUZIMPL3:7;
ex f, g being Function of [.0,1.],REAL st
( f = N1 & g = N2 & EX = min (f,g) ) ;
hence ex b₁ being Fuzzy_Negation ex f, g being Function of [.0,1.],REAL st
( f = N1 & g = N2 & b₁ = min (f,g) ) ; :: thesis: verum