set f = kappa R;
let X, Y, Z be Subset of R; ROUGHIF1:def 8 ( Y c= Z implies (kappa R) . (X,Y) <= (kappa R) . (X,Z) )
assume
Y c= Z
; (kappa R) . (X,Y) <= (kappa R) . (X,Z)
then
kappa (X,Y) <= kappa (X,Z)
by Prop1b;
then
(kappa R) . (X,Y) <= kappa (X,Z)
by DefKappa;
hence
(kappa R) . (X,Y) <= (kappa R) . (X,Z)
by DefKappa; verum