let R be finite Approximation_Space; :: thesis: for X, Y, Z being Subset of R st Y c= Z holds
kappa_2 (X,Y) <= kappa_2 (X,Z)
let X, Y, Z be Subset of R; :: thesis: ( Y c= Z implies kappa_2 (X,Y) <= kappa_2 (X,Z) )
assume Y c= Z ; :: thesis: kappa_2 (X,Y) <= kappa_2 (X,Z)
then (X `) \/ Y c= (X `) \/ Z by XBOOLE_1:9;
hence kappa_2 (X,Y) <= kappa_2 (X,Z) by XREAL_1:72, NAT_1:43; :: thesis: verum