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