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;