let R be finite Approximation_Space; :: thesis: for X, Y, Z being Subset of R st Y c= Z holds
kappa_1 (X,Y) <= kappa_1 (X,Z)
let X, Y, Z be Subset of R; :: thesis: ( Y c= Z implies kappa_1 (X,Y) <= kappa_1 (X,Z) )
assume A0: Y c= Z ; :: thesis: kappa_1 (X,Y) <= kappa_1 (X,Z)
then B3: card Z = card (Y \/ (Z \ Y)) by XBOOLE_1:45
.= (card Y) + (card (Z \ Y)) by XBOOLE_1:79, CARD_2:40 ;
ZA: card Y <= card (X \/ Y) by NAT_1:43, XBOOLE_1:7;
ZC: X \/ Z = X \/ (Y \/ (Z \ Y)) by A0, XBOOLE_1:45
.= (X \/ Y) \/ (Z \ Y) by XBOOLE_1:4 ;

per cases ( X \/ Y <> {} or ( X = {} & Z = {} ) or ( X \/ Y = {} & Z <> {} ) ) ;

suppose AA: X \/ Y <> {} ; :: thesis: kappa_1 (X,Y) <= kappa_1 (X,Z)

then kappa_1 (X,Y) = (card Y) / (card (X \/ Y)) by Kappa1;
then ss: kappa_1 (X,Y) <= ((card Y) + (card (Z \ Y))) / ((card (X \/ Y)) + (card (Z \ Y))) by AA, Lemacik, ZA;
(card Z) / ((card (X \/ Y)) + (card (Z \ Y))) <= (card Z) / (card ((X \/ Y) \/ (Z \ Y))) by CARD_2:43, AA, XREAL_1:118;
then kappa_1 (X,Y) <= (card Z) / (card ((X \/ Y) \/ (Z \ Y))) by ss, B3, XXREAL_0:2;
hence kappa_1 (X,Y) <= kappa_1 (X,Z) by Kappa1, AA, ZC; :: thesis: verum

end;

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

hence kappa_1 (X,Y) <= kappa_1 (X,Z) by A0; :: thesis: verum

end;

suppose T1: ( X \/ Y = {} & Z <> {} ) ; :: thesis: kappa_1 (X,Y) <= kappa_1 (X,Z)

then T3: ( X \/ Z <> {} & X = {} ) ;
kappa_1 (X,Z) = (card Z) / (card (X \/ Z)) by Kappa1, T1
.= 1 by XCMPLX_1:60, T3 ;
hence kappa_1 (X,Y) <= kappa_1 (X,Z) by T1, Kappa1; :: thesis: verum

end;

end;