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

proof

let x, y be Element of X; :: according to LFUZZY_1:def 5 :: thesis: (Zmf (X,X)) . (x,y) = (Zmf (X,X)) . (y,x)
( (Zmf (X,X)) . [x,y] = 0 & (Zmf (X,X)) . [y,x] = 0 ) by FUZZY_4:21;
hence (Zmf (X,X)) . (x,y) = (Zmf (X,X)) . (y,x) ; :: thesis: verum

end;

thus Zmf (X,X) is antisymmetric :: thesis: Zmf (X,X) is transitive

proof

let x, y be Element of X; :: according to LFUZZY_1:def 8 :: thesis: ( (Zmf (X,X)) . (x,y) <> 0 & (Zmf (X,X)) . (y,x) <> 0 implies x = y )
(Zmf (X,X)) . [x,y] = 0 by FUZZY_4:21;
hence ( (Zmf (X,X)) . (x,y) <> 0 & (Zmf (X,X)) . (y,x) <> 0 implies x = y ) ; :: thesis: verum

end;

thus Zmf (X,X) is transitive :: thesis: verum

proof

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

end;