let X, Y be Subset of ExampleRIFSpace; :: thesis: ( X = {1,2} & Y = {2,3,4} implies kappa (X,Y), kappa_1 (X,Y), kappa_2 (X,Y) are_mutually_distinct )
assume A1: ( X = {1,2} & Y = {2,3,4} ) ; :: thesis: kappa (X,Y), kappa_1 (X,Y), kappa_2 (X,Y) are_mutually_distinct
then A3: card Y = 3 by CARD_2:58;
set U = the carrier of ExampleRIFSpace;
1,2,3,4,5 are_mutually_distinct by ZFMISC_1:def 7;
then a1: card the carrier of ExampleRIFSpace = 5 by CARD_2:63;
( 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;
a5: X \/ Y = {1,2} \/ ({2} \/ {3,4}) by A1, ENUMSET1:2
.= ({1,2} \/ {2}) \/ {3,4} by XBOOLE_1:4
.= {1,2} \/ {3,4} by ZFMISC_1:9
.= {1,2,3,4} by ENUMSET1:5 ;
( not 1 in {3,4,5} & not 2 in {3,4,5} ) by ENUMSET1:def 1;
then W2: {1,2} misses {3,4,5} by ZFMISC_1:51;
WW: ( 3 in {3,4,5} & 4 in {3,4,5} ) by ENUMSET1:def 1;
X ` = ({1,2} \/ {3,4,5}) \ {1,2} by A1, ENUMSET1:8
.= {3,4,5} by XBOOLE_1:88, W2 ;
then (X `) \/ Y = {3,4,5} \/ ({2} \/ {3,4}) by A1, ENUMSET1:2
.= {2} \/ ({3,4} \/ {3,4,5}) by XBOOLE_1:4
.= {2} \/ {3,4,5} by ZFMISC_1:42, WW ;
then (X `) \/ Y = {2,3,4,5} by ENUMSET1:4;
then W3: (card ((X `) \/ Y)) / (card the carrier of ExampleRIFSpace) = 4 / 5 by a1, CARD_2:59;
W4: kappa (X,Y) = (card (X /\ Y)) / (card X) by KappaDef, A1
.= 1 / 2 by A4, A1, CARD_2:57 ;
kappa_1 (X,Y) = (card Y) / (card (X \/ Y)) by Kappa1, A1
.= 3 / 4 by A3, a5, CARD_2:59 ;
hence kappa (X,Y), kappa_1 (X,Y), kappa_2 (X,Y) are_mutually_distinct by ZFMISC_1:def 5, W4, W3; :: thesis: verum