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

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