let R be finite Approximation_Space; :: thesis: for X, Y being Subset of R st X \/ Y = [#] R holds
kappa_1 (X,Y) = kappa_2 (X,Y)
let X, Y be Subset of R; :: thesis: ( X \/ Y = [#] R implies kappa_1 (X,Y) = kappa_2 (X,Y) )
assume AB: X \/ Y = [#] R ; :: thesis: kappa_1 (X,Y) = kappa_2 (X,Y)
((X `) `) \/ Y = [#] R by AB;
then F1: card Y = card ((X `) \/ Y) by XBOOLE_1:12, LemmaSet;
per cases ( X \/ Y <> {} or X \/ Y = {} ) ;
suppose X \/ Y <> {} ; :: thesis: kappa_1 (X,Y) = kappa_2 (X,Y)
thus kappa_1 (X,Y) = kappa_2 (X,Y) by F1, AB, Kappa1; :: thesis: verum
end;
suppose X \/ Y = {} ; :: thesis: kappa_1 (X,Y) = kappa_2 (X,Y)
hence kappa_1 (X,Y) = kappa_2 (X,Y) by AB; :: thesis: verum
end;
end;