let R be finite Approximation_Space; :: thesis: for X, Y being Subset of R st ( ( X = {} & Y <> {} ) or ( X <> {} & Y = {} ) ) holds
((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) = 1
let X, Y be Subset of R; :: thesis: ( ( ( X = {} & Y <> {} ) or ( X <> {} & Y = {} ) ) implies ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) = 1 )
assume ( ( X = {} & Y <> {} ) or ( X <> {} & Y = {} ) ) ; :: thesis: ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) = 1
per cases then ( ( X = {} & Y <> {} ) or ( Y = {} & X <> {} ) ) ;
suppose A0: ( X = {} & Y <> {} ) ; :: thesis: ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) = 1
then ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) = ((card (X \ Y)) / (card (X \/ Y))) + ((CMap (kappa_1 R)) . (Y,X)) by PropEx3
.= ((card (X \ Y)) / (card (X \/ Y))) + ((card (Y \ X)) / (card (X \/ Y))) by PropEx3, A0
.= (card Y) / (card Y) by A0 ;
hence ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) = 1 by A0, XCMPLX_1:60; :: thesis: verum
end;
suppose A0: ( Y = {} & X <> {} ) ; :: thesis: ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) = 1
then ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) = ((card (X \ Y)) / (card (X \/ Y))) + ((CMap (kappa_1 R)) . (Y,X)) by PropEx3
.= ((card (X \ Y)) / (card (X \/ Y))) + ((card (Y \ X)) / (card (X \/ Y))) by PropEx3, A0
.= (card X) / (card X) by A0 ;
hence ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X)) = 1 by A0, XCMPLX_1:60; :: thesis: verum
end;
end;