set f = kappa_1 R;
let X, Y, Z be Subset of R; :: according to ROUGHIF1:def 8 :: thesis: ( Y c= Z implies (kappa_1 R) . (X,Y) <= (kappa_1 R) . (X,Z) )
assume Y c= Z ; :: thesis: (kappa_1 R) . (X,Y) <= (kappa_1 R) . (X,Z)
then kappa_1 (X,Y) <= kappa_1 (X,Z) by Prop2b;
then (kappa_1 R) . (X,Y) <= kappa_1 (X,Z) by DefKappa1;
hence (kappa_1 R) . (X,Y) <= (kappa_1 R) . (X,Z) by DefKappa1; :: thesis: verum