let R be finite Approximation_Space; 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; ( kappa (X,Y) <= kappa_1 (X,Y) & kappa_1 (X,Y) <= kappa_2 (X,Y) )
per cases
( X <> {} or X = {} )
;
suppose A0:
X <> {}
;
( 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;
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;
verum end;