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;