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;