let R be finite Approximation_Space; :: thesis: for X being Subset of R st X <> {} holds
kappa (X,({} R)) = 0
let X be Subset of R; :: thesis: ( X <> {} implies kappa (X,({} R)) = 0 )
assume X <> {} ; :: thesis: kappa (X,({} R)) = 0
then kappa (X,({} R)) = (card (X /\ ({} R))) / (card X) by KappaDef;
hence kappa (X,({} R)) = 0 ; :: thesis: verum