let R be finite Approximation_Space; :: thesis: for X, Y being Subset of R holds
( kappa_2 (X,Y) = 1 iff X c= Y )
let X, Y be Subset of R; :: thesis: ( kappa_2 (X,Y) = 1 iff X c= Y )
thus ( kappa_2 (X,Y) = 1 implies X c= Y ) :: thesis: ( X c= Y implies kappa_2 (X,Y) = 1 )
proof
assume kappa_2 (X,Y) = 1 ; :: thesis: X c= Y
then card ((X `) \/ Y) = card ([#] R) by XCMPLX_1:58;
hence X c= Y by LemmaSet, LemmaCard2; :: thesis: verum
end;
assume X c= Y ; :: thesis: kappa_2 (X,Y) = 1
then (X `) \/ Y = [#] R by LemmaSet;
hence kappa_2 (X,Y) = 1 by XCMPLX_1:60; :: thesis: verum