let R be finite Approximation_Space; :: thesis: for X, Y being Subset of R holds
( kappa (X,Y) = 1 iff X c= Y )
let X, Y be Subset of R; :: thesis: ( kappa (X,Y) = 1 iff X c= Y )

per cases ( X <> {} or X = {} ) ;

suppose A1: X <> {} ; :: thesis: ( kappa (X,Y) = 1 iff X c= Y )

thus ( kappa (X,Y) = 1 implies X c= Y ) :: thesis: ( X c= Y implies kappa (X,Y) = 1 )

proof

assume kappa (X,Y) = 1 ; :: thesis: X c= Y
then (card (X /\ Y)) / (card X) = 1 by KappaDef, A1;
then card (X /\ Y) = card X by XCMPLX_1:58;
then X /\ Y = X by CARD_2:102, XBOOLE_1:17;
hence X c= Y by XBOOLE_1:17; :: thesis: verum

end;

assume X c= Y ; :: thesis: kappa (X,Y) = 1
then X /\ Y = X by XBOOLE_1:28;
then kappa (X,Y) = (card X) / (card X) by A1, KappaDef;
hence kappa (X,Y) = 1 by XCMPLX_1:60, A1; :: thesis: verum

end;

suppose X = {} ; :: thesis: ( kappa (X,Y) = 1 iff X c= Y )

hence ( kappa (X,Y) = 1 iff X c= Y ) by KappaDef; :: thesis: verum

end;

end;