let R be finite Approximation_Space; :: thesis: for X, Y being Subset of R st X <> {} holds
( kappa_1 (X,Y) = 0 iff Y = {} )
let X, Y be Subset of R; :: thesis: ( X <> {} implies ( kappa_1 (X,Y) = 0 iff Y = {} ) )
assume a3: X <> {} ; :: thesis: ( kappa_1 (X,Y) = 0 iff Y = {} )
thus ( kappa_1 (X,Y) = 0 implies Y = {} ) by LemmaProp4a; :: thesis: ( Y = {} implies kappa_1 (X,Y) = 0 )
assume A2: Y = {} ; :: thesis: kappa_1 (X,Y) = 0
kappa_1 (X,Y) = (card Y) / (card (X \/ Y)) by Kappa1, a3
.= 0 / (card (X \/ Y)) by A2 ;
hence kappa_1 (X,Y) = 0 ; :: thesis: verum