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

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

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

then kappa (Y,Z) = (card (Y /\ Z)) / (card Y) by KappaDef;
then F1: kappa (Y,Z) = (card Z) / (card Y) by AA, XBOOLE_1:28;
Z c= X by AA;
then e2: X /\ Z = Z by XBOOLE_1:28;
kappa (X,Z) = (card Z) / (card X) by e2, A1, KappaDef;
hence kappa (X,Z) <= kappa (Y,Z) by A1, XREAL_1:118, F1, AA, NAT_1:43; :: thesis: verum

end;

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

hence kappa (X,Z) <= kappa (Y,Z) by AA; :: thesis: verum

end;

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

hence kappa (X,Z) <= kappa (Y,Z) ; :: thesis: verum

end;

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

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

end;

end;