let R be finite Approximation_Space; :: thesis: for X, Y being Subset of R holds kappa_2 (X,Y) = kappa (([#] R),((X `) \/ Y))
let X, Y be Subset of R; :: thesis: kappa_2 (X,Y) = kappa (([#] R),((X `) \/ Y))
kappa (([#] R),((X `) \/ Y)) = (card (([#] R) /\ ((X `) \/ Y))) / (card ([#] R)) by KappaDef
.= (card ((X `) \/ Y)) / (card ([#] R)) ;
hence kappa_2 (X,Y) = kappa (([#] R),((X `) \/ Y)) ; :: thesis: verum