let X, Y, U be Subset of ExampleRIFSpace; :: thesis: ( X = {1,2} & Y = {1,2,3} & U = {2,4,5} implies not kappa (X,U) <= kappa (Y,U) )
assume A1: ( X = {1,2} & Y = {1,2,3} & U = {2,4,5} ) ; :: thesis: not kappa (X,U) <= kappa (Y,U)
then A3: card Y = 3 by CARD_2:58;
( 2 in U & not 1 in U ) by A1, ENUMSET1:def 1;
then X /\ U = {2} by A1, ZFMISC_1:54;
then R1: card (X /\ U) = 1 by CARD_1:30;
R2: card X = 2 by CARD_2:57, A1;
R0: U = {2} \/ {4,5} by A1, ENUMSET1:2;
ro: 2 in Y by A1, ENUMSET1:def 1;
w1: not 4 in Y by A1, ENUMSET1:def 1;
not 5 in Y by A1, ENUMSET1:def 1;
then rr: Y misses {4,5} by ZFMISC_1:51, w1;
Y /\ U = (Y /\ {2}) \/ (Y /\ {4,5}) by R0, XBOOLE_1:23
.= Y /\ {2} by rr ;
then Y /\ U = {2} by XBOOLE_1:28, ro, ZFMISC_1:31;
then R3: card (Y /\ U) = 1 by CARD_1:30;
W4: kappa (X,U) = 1 / 2 by R1, R2, A1, KappaDef;
kappa (Y,U) = 1 / 3 by A3, R3, A1, KappaDef;
hence not kappa (X,U) <= kappa (Y,U) by W4; :: thesis: verum