let R be finite Approximation_Space; :: thesis: for X being Subset of R holds kappa_2 (({} R),X) = 1
let X be Subset of R; :: thesis: kappa_2 (({} R),X) = 1
{} R c= X ;
hence kappa_2 (({} R),X) = 1 by Prop11b; :: thesis: verum