let R be finite Approximation_Space; for X, Y being Subset of R st X <> {} holds
( kappa (X,Y) = 0 iff X misses Y )
let X, Y be Subset of R; ( X <> {} implies ( kappa (X,Y) = 0 iff X misses Y ) )
assume AA:
X <> {}
; ( kappa (X,Y) = 0 iff X misses Y )
thus
( kappa (X,Y) = 0 implies X misses Y )
by LemmaProp2b; ( X misses Y implies kappa (X,Y) = 0 )
assume
X misses Y
; kappa (X,Y) = 0
then
(card (X /\ Y)) / (card X) = 0
;
hence
kappa (X,Y) = 0
by AA, KappaDef; verum