let R be finite Approximation_Space; :: thesis: for X, Y being Subset of R holds
( kappa (X,Y) <= kappa_1 (X,Y) & kappa_1 (X,Y) <= kappa_2 (X,Y) )
let X, Y be Subset of R; :: thesis: ( kappa (X,Y) <= kappa_1 (X,Y) & kappa_1 (X,Y) <= kappa_2 (X,Y) )

per cases ( X <> {} or X = {} ) ;

suppose A0: X <> {} ; :: thesis: ( kappa (X,Y) <= kappa_1 (X,Y) & kappa_1 (X,Y) <= kappa_2 (X,Y) )

then WA: kappa_1 (X,Y) = (card Y) / (card (X \/ Y)) by Kappa1;
U1: card (X /\ Y) <= card X by NAT_1:43, XBOOLE_1:17;
J0: card Y <= card (X \/ Y) by NAT_1:43, XBOOLE_1:7;
X \/ Y = X \/ (Y \ X) by XBOOLE_1:39;
then D3: card (X \/ Y) = (card X) + (card (Y \ X)) by CARD_2:40, XBOOLE_1:85;
d4: Y = (X /\ Y) \/ (Y \ X) by XBOOLE_1:51;
X /\ Y misses Y \ X by XBOOLE_1:85, XBOOLE_1:17;
then D4: card Y = (card (X /\ Y)) + (card (Y \ X)) by d4, CARD_2:40;
(X \/ Y) ` = (X `) /\ (Y `) by XBOOLE_1:53;
then ((X \/ Y) `) \/ Y = ((X `) \/ Y) /\ ((Y `) \/ Y) by XBOOLE_1:24
.= ((X `) \/ Y) /\ ([#] R) by PRE_TOPC:2
.= ((X `) \ Y) \/ Y by XBOOLE_1:39 ;
then d5: ( (X `) \/ Y = ((X `) \ Y) \/ Y & ((X `) \ Y) \/ Y = ((X \/ Y) `) \/ Y ) by XBOOLE_1:39;
(X \/ Y) ` c= Y ` by SUBSET_1:12, XBOOLE_1:7;
then (X \/ Y) ` misses Y by XBOOLE_1:63, XBOOLE_1:79;
then D5: card ((X `) \/ Y) = (card ((X \/ Y) `)) + (card Y) by d5, CARD_2:40;
(card (X /\ Y)) / (card X) <= ((card (X /\ Y)) + (card (Y \ X))) / ((card X) + (card (Y \ X))) by Lemacik, A0, U1;
then kappa (X,Y) <= ((card (X /\ Y)) + (card (Y \ X))) / (card (X \/ Y)) by A0, KappaDef, D3;
hence kappa (X,Y) <= kappa_1 (X,Y) by A0, Kappa1, D4; :: thesis: kappa_1 (X,Y) <= kappa_2 (X,Y)
((X \/ Y) `) \/ (X \/ Y) = [#] R by PRE_TOPC:2;
then (card ((X \/ Y) `)) + (card (X \/ Y)) = card ([#] R) by TDLAT_1:2, CARD_2:40;
hence kappa_1 (X,Y) <= kappa_2 (X,Y) by D5, A0, J0, Lemacik, WA; :: thesis: verum

end;

suppose X = {} ; :: thesis: ( kappa (X,Y) <= kappa_1 (X,Y) & kappa_1 (X,Y) <= kappa_2 (X,Y) )

then b3: X = {} R ;
then kappa_1 (X,Y) = 1 by Lemma2;
hence ( kappa (X,Y) <= kappa_1 (X,Y) & kappa_1 (X,Y) <= kappa_2 (X,Y) ) by b3, Lemma3, KappaDef; :: thesis: verum

end;

end;