let X, Y be Subset of ExampleRIFSpace; :: thesis: ( X = {1,2} & Y = {2,3,4} implies kappa (X,Y) <> kappa (Y,X) )
assume A1: ( X = {1,2} & Y = {2,3,4} ) ; :: thesis: 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; :: thesis: verum