let fi be Fuzzy_Implication; :: thesis: fi <= I_{1}
set f = I_{1} ;
for x, y being Element of [.0,1.] holds I_{1} . (x,y) >= fi . (x,y)

proof

let x, y be Element of [.0,1.]; :: thesis: I_{1} . (x,y) >= fi . (x,y)
a0: ( x <= 1 & y >= 0 ) by XXREAL_1:1;

per cases ( x <> 1 or y <> 0 or ( x = 1 & y = 0 ) ) ;

suppose ( x <> 1 or y <> 0 ) ; :: thesis: I_{1} . (x,y) >= fi . (x,y)

then ( x < 1 or y > 0 ) by a0, XXREAL_0:1;
then I_{1} . (x,y) = 1 by I1Impl;
hence I_{1} . (x,y) >= fi . (x,y) by XXREAL_1:1; :: thesis: verum

end;

suppose Aa: ( x = 1 & y = 0 ) ; :: thesis: I_{1} . (x,y) >= fi . (x,y)

then I_{1} . (x,y) = 0 by I1Impl;
hence I_{1} . (x,y) >= fi . (x,y) by Aa, Def10; :: thesis: verum

end;

end;

end;

hence fi <= I_{1} by FUZNORM1:def 16; :: thesis: verum