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= ;
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;
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;