let X be non empty set ; :: thesis: ( Umf X,X is symmetric & Umf X,X is transitive & Umf X,X is reflexive )
thus Umf X,X is symmetric :: thesis: ( Umf X,X is transitive & Umf X,X is reflexive )

proof

let x, y be Element of X; :: according to LFUZZY_1:def 5 :: thesis: (Umf X,X) . x,y = (Umf X,X) . y,x
thus (Umf X,X) . x,y = (Umf X,X) . [x,y]
.= 1 by FUZZY_4:21
.= (Umf X,X) . [y,x] by FUZZY_4:21
.= (Umf X,X) . y,x ; :: thesis: verum

end;

thus Umf X,X is transitive :: thesis: Umf X,X is reflexive

proof

let x, y, z be Element of X; :: according to LFUZZY_1:def 7 :: thesis: ((Umf X,X) . [x,y]) "/\" ((Umf X,X) . [y,z]) <<= (Umf X,X) . [x,z]
((Umf X,X) . [x,y]) "/\" ((Umf X,X) . [y,z]) = min 1,((Umf X,X) . [y,z]) by FUZZY_4:20
.= min 1,1 by FUZZY_4:20
.= 1 ;
then ((Umf X,X) . [x,y]) "/\" ((Umf X,X) . [y,z]) <= (Umf X,X) . [x,z] by FUZZY_4:20;
hence ((Umf X,X) . [x,y]) "/\" ((Umf X,X) . [y,z]) <<= (Umf X,X) . [x,z] by LFUZZY_0:3; :: thesis: verum

end;

thus Umf X,X is reflexive :: thesis: verum

proof

let x be Element of X; :: according to LFUZZY_1:def 3 :: thesis: (Umf X,X) . x,x = 1
(Umf X,X) . [x,x] = 1 by FUZZY_4:21;
hence (Umf X,X) . x,x = 1 ; :: thesis: verum

end;