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

proof

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

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

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

then I_{0} . (x,y) = 1 by LBProp, RBProp;
hence I_{0} . (x,y) <= fi . (x,y) by LBProp, RBProp, A1; :: thesis: verum

end;

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

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

end;

end;

end;

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