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

assume A2:
for x being Element of X holds R . (x,x) = 1
; :: thesis: R is reflexive assume
R is reflexive
; :: thesis: for x being Element of X holds R . (x,x) = 1

then A1: R c= ;

thus for x being Element of X holds R . (x,x) = 1 :: thesis: verum

end;then A1: R c= ;

thus for x being Element of X holds R . (x,x) = 1 :: thesis: verum

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)