let R be finite Approximation_Space; :: thesis: for X, Y being Subset of R st kappa (X,Y) = 0 holds
X misses Y
let X, Y be Subset of R; :: thesis: ( kappa (X,Y) = 0 implies X misses Y )
assume A1: kappa (X,Y) = 0 ; :: thesis: X misses Y

per cases ( X <> {} or X = {} ) ;

suppose A2: X <> {} ; :: thesis: X misses Y

then kappa (X,Y) = (card (X /\ Y)) / (card X) by KappaDef;
hence X misses Y by A1, A2; :: thesis: verum

end;

suppose X = {} ; :: thesis: X misses Y

hence X misses Y ; :: thesis: verum

end;

end;