set f = kappa R;
let X, Y, Z be Subset of R; :: according to ROUGHIF1:def 8 :: thesis: ( Y c= Z implies (kappa R) . (X,Y) <= (kappa R) . (X,Z) )
assume Y c= Z ; :: thesis: (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; :: thesis: verum