let X, Y be Subset of R; :: according to ROUGHIF1:def 10 :: thesis: ( (kappa_2 R) . (X,Y) = 0 implies X misses Y )
assume (kappa_2 R) . (X,Y) = 0 ; :: thesis: X misses Y
then kappa_2 (X,Y) = 0 by DefKappa2;
hence X misses Y by Kappa2RIF4; :: thesis: verum