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 )

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

proof

thus
Zmf (X,X) is antisymmetric
:: thesis: Zmf (X,X) is transitive
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;( (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

proof

thus
Zmf (X,X) is transitive
:: thesis: verum
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;(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

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