let R be finite Approximation_Space; :: thesis: for X, Y, Z being Subset of R st Y c= Z holds
kappa (X,Y) <= kappa (X,Z)
let X, Y, Z be Subset of R; :: thesis: ( Y c= Z implies kappa (X,Y) <= kappa (X,Z) )
assume A0: Y c= Z ; :: thesis: kappa (X,Y) <= kappa (X,Z)

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

suppose A1: X <> {} ; :: thesis: kappa (X,Y) <= kappa (X,Z)

card (X /\ Y) <= card (X /\ Z) by NAT_1:43, A0, XBOOLE_1:26;
then (card (X /\ Y)) / (card X) <= (card (X /\ Z)) / (card X) by XREAL_1:72;
then kappa (X,Y) <= (card (X /\ Z)) / (card X) by A1, KappaDef;
hence kappa (X,Y) <= kappa (X,Z) by A1, KappaDef; :: thesis: verum

end;

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

then ( kappa (X,Y) = 1 & kappa (X,Z) = 1 ) by KappaDef;
hence kappa (X,Y) <= kappa (X,Z) ; :: thesis: verum

end;

end;