let R be finite Approximation_Space; :: thesis: for X, Y being Subset of R holds
( kappa_2 (X,Y) = 0 iff ( X = [#] R & Y = {} ) )
let X, Y be Subset of R; :: thesis: ( kappa_2 (X,Y) = 0 iff ( X = [#] R & Y = {} ) )
thus ( kappa_2 (X,Y) = 0 implies ( X = [#] R & Y = {} ) ) :: thesis: ( X = [#] R & Y = {} implies kappa_2 (X,Y) = 0 )
proof
assume ac: kappa_2 (X,Y) = 0 ; :: thesis: ( X = [#] R & Y = {} )
then ( X ` = {} & Y = {} ) ;
then (X `) ` = ({} R) ` ;
hence ( X = [#] R & Y = {} ) by ac; :: thesis: verum
end;
assume A2: ( X = [#] R & Y = {} ) ; :: thesis: kappa_2 (X,Y) = 0
then X ` = (({} R) `) ` ;
hence kappa_2 (X,Y) = 0 by A2; :: thesis: verum