let fi be Fuzzy_Implication; :: thesis: for y being Element of [.0,1.] holds fi . (0,y) = 1
let y be Element of [.0,1.]; :: thesis: fi . (0,y) = 1
A1: fi . (0,0) = 1 by Def00;
B1: 0 in [.0,1.] by XXREAL_1:1;
reconsider z = 0 as Element of [.0,1.] by XXREAL_1:1;
0 <= y by XXREAL_1:1;
then B2: fi . (0,0) <= fi . (0,y) by DefIncr, B1;
fi . (z,y) in [.0,1.] ;
then fi . (0,y) <= 1 by XXREAL_1:1;
hence fi . (0,y) = 1 by XXREAL_0:1, A1, B2; :: thesis: verum