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