let X, Y be Subset of ExampleRIFSpace; ( X = {1,2} & Y = {2,3,4} implies kappa (X,Y) <> kappa (Y,X) )
assume A1:
( X = {1,2} & Y = {2,3,4} )
; kappa (X,Y) <> kappa (Y,X)
then A3:
card Y = 3
by CARD_2:58;
Z1:
kappa (Y,X) = (card (Y /\ X)) / (card Y)
by KappaDef, A1;
set U = the carrier of ExampleRIFSpace;
( 2 in Y & not 1 in Y )
by A1, ENUMSET1:def 1;
then
X /\ Y = {2}
by ZFMISC_1:54, A1;
then A4:
card (X /\ Y) = 1
by CARD_1:30;
kappa (X,Y) =
(card (X /\ Y)) / (card X)
by KappaDef, A1
.=
1 / 2
by A4, A1, CARD_2:57
;
hence
kappa (X,Y) <> kappa (Y,X)
by A3, Z1, A4; verum