hereby :: thesis: ( ( for x being Element of X holds R . x,x = 1 ) implies R is reflexive )

assume R is reflexive ; :: thesis: for x being Element of X holds R . x,x = 1
then A1: R c= by Def2;
thus for x being Element of X holds R . x,x = 1 :: thesis: verum

proof

let x be Element of X; :: thesis: R . x,x = 1
(Imf X,X) . x,x <= R . x,x by A1, Def1;
then ( R . x,x <= 1 & R . x,x >= 1 ) by FUZZY_4:4, FUZZY_4:25;
hence R . x,x = 1 by XXREAL_0:1; :: thesis: verum

end;

end;

assume A2: for x being Element of X holds R . x,x = 1 ; :: thesis: R is reflexive
let x, y be Element of X; :: according to LFUZZY_1:def 1,LFUZZY_1:def 2 :: thesis: (Imf X,X) . x,y <= R . x,y

per cases ( x = y or x <> y ) ;

suppose A3: x = y ; :: thesis: (Imf X,X) . x,y <= R . x,y

then (Imf X,X) . x,y = 1 by FUZZY_4:25;
hence (Imf X,X) . x,y <= R . x,y by A2, A3; :: thesis: verum

end;

suppose x <> y ; :: thesis: (Imf X,X) . x,y <= R . x,y

then (Imf X,X) . x,y = 0 by FUZZY_4:25;
hence (Imf X,X) . x,y <= R . x,y by FUZZY_4:4; :: thesis: verum

end;

end;