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