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

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

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

then Y = {} by A1, Prop4a;
hence X misses Y ; :: thesis: verum

end;

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

hence X misses Y ; :: thesis: verum

end;

end;