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