let X be non empty set ; ( Zmf (X,X) is symmetric & Zmf (X,X) is antisymmetric & Zmf (X,X) is transitive )
thus
Zmf (X,X) is symmetric
( Zmf (X,X) is antisymmetric & Zmf (X,X) is transitive )proof
let x,
y be
Element of
X;
LFUZZY_1:def 5 (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)
;
verum
end;
thus
Zmf (X,X) is antisymmetric
Zmf (X,X) is transitive proof
let x,
y be
Element of
X;
LFUZZY_1:def 8 ( (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 )
;
verum
end;
thus
Zmf (X,X) is transitive
verumproof
let x,
y,
z be
Element of
X;
LFUZZY_1:def 7 ((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;
verum
end;