let fi be Fuzzy_Implication; :: thesis: for x being Element of [.0,1.] holds fi . (x,1) = 1

let x be Element of [.0,1.]; :: thesis: fi . (x,1) = 1

A1: fi . (1,1) = 1 by Def11;

B1: 1 in [.0,1.] by XXREAL_1:1;

reconsider z = 1 as Element of [.0,1.] by XXREAL_1:1;

x <= 1 by XXREAL_1:1;

then B2: fi . (1,1) <= fi . (x,1) by DefDecr, B1;

fi . (x,z) in [.0,1.] ;

then fi . (x,1) <= 1 by XXREAL_1:1;

hence fi . (x,1) = 1 by XXREAL_0:1, A1, B2; :: thesis: verum

let x be Element of [.0,1.]; :: thesis: fi . (x,1) = 1

A1: fi . (1,1) = 1 by Def11;

B1: 1 in [.0,1.] by XXREAL_1:1;

reconsider z = 1 as Element of [.0,1.] by XXREAL_1:1;

x <= 1 by XXREAL_1:1;

then B2: fi . (1,1) <= fi . (x,1) by DefDecr, B1;

fi . (x,z) in [.0,1.] ;

then fi . (x,1) <= 1 by XXREAL_1:1;

hence fi . (x,1) = 1 by XXREAL_0:1, A1, B2; :: thesis: verum