let R be finite Approximation_Space; for X, Y being Subset of R st ( ( X = {} & Y <> {} ) or ( X <> {} & Y = {} ) ) holds
( ((CMap (kappa R)) . (X,Y)) + ((CMap (kappa R)) . (Y,X)) = ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) & ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) = 1 )
let X, Y be Subset of R; ( ( ( X = {} & Y <> {} ) or ( X <> {} & Y = {} ) ) implies ( ((CMap (kappa R)) . (X,Y)) + ((CMap (kappa R)) . (Y,X)) = ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) & ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) = 1 ) )
assume A1:
( ( X = {} & Y <> {} ) or ( X <> {} & Y = {} ) )
; ( ((CMap (kappa R)) . (X,Y)) + ((CMap (kappa R)) . (Y,X)) = ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) & ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) = 1 )
then
((CMap (kappa R)) . (X,Y)) + ((CMap (kappa R)) . (Y,X)) = 1
by Lemma6f;
hence
( ((CMap (kappa R)) . (X,Y)) + ((CMap (kappa R)) . (Y,X)) = ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) & ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) = 1 )
by A1, Lemma6f1; verum