let R be finite Approximation_Space; :: thesis: for X, Y being Subset of R holds
( kappa_1 (X,Y) = 1 iff X c= Y )
let X, Y be Subset of R; :: thesis: ( kappa_1 (X,Y) = 1 iff X c= Y )
per cases ( ( X \/ Y <> {} & Y <> {} ) or ( X \/ Y <> {} & Y = {} ) or X \/ Y = {} ) ;
suppose A1: ( X \/ Y <> {} & Y <> {} ) ; :: thesis: ( kappa_1 (X,Y) = 1 iff X c= Y )
then B1: kappa_1 (X,Y) = (card Y) / (card (X \/ Y)) by Kappa1;
thus ( kappa_1 (X,Y) = 1 implies X c= Y ) :: thesis: ( X c= Y implies kappa_1 (X,Y) = 1 )
proof
assume kappa_1 (X,Y) = 1 ; :: thesis: X c= Y
then card Y = card (X \/ Y) by XCMPLX_1:58, B1;
hence X c= Y by LemmaCard; :: thesis: verum
end;
assume X c= Y ; :: thesis: kappa_1 (X,Y) = 1
then card (X \/ Y) = card Y by XBOOLE_1:12;
hence kappa_1 (X,Y) = 1 by A1, XCMPLX_1:60, B1; :: thesis: verum
end;
suppose A1: ( X \/ Y <> {} & Y = {} ) ; :: thesis: ( kappa_1 (X,Y) = 1 iff X c= Y )
then kappa_1 (X,Y) = (card Y) / (card (X \/ Y)) by Kappa1
.= 0 by A1 ;
hence ( kappa_1 (X,Y) = 1 iff X c= Y ) by A1; :: thesis: verum
end;
suppose X \/ Y = {} ; :: thesis: ( kappa_1 (X,Y) = 1 iff X c= Y )
hence ( kappa_1 (X,Y) = 1 iff X c= Y ) by Kappa1; :: thesis: verum
end;
end;