let R be finite Approximation_Space; :: thesis: for X, Y, Z being Subset of R holds ((delta_1 R) . (X,Y)) + ((delta_1 R) . (Y,Z)) >= (delta_1 R) . (X,Z)
let X, Y, Z be Subset of R; :: thesis: ((delta_1 R) . (X,Y)) + ((delta_1 R) . (Y,Z)) >= (delta_1 R) . (X,Z)
set m1 = (CMap (kappa_1 R)) . (X,Y);
set m2 = (CMap (kappa_1 R)) . (Y,Z);
set m3 = (CMap (kappa_1 R)) . (X,Z);
set m4 = (CMap (kappa_1 R)) . (Z,Y);
set m5 = (CMap (kappa_1 R)) . (Y,X);
set m6 = (CMap (kappa_1 R)) . (Z,X);
A1: ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,Z)) >= (CMap (kappa_1 R)) . (X,Z) by Prop6d1;
((CMap (kappa_1 R)) . (Z,Y)) + ((CMap (kappa_1 R)) . (Y,X)) >= (CMap (kappa_1 R)) . (Z,X) by Prop6d1;
then (((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,Z))) + (((CMap (kappa_1 R)) . (Z,Y)) + ((CMap (kappa_1 R)) . (Y,X))) >= ((CMap (kappa_1 R)) . (X,Z)) + ((CMap (kappa_1 R)) . (Z,X)) by A1, XREAL_1:7;
then (((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,X))) + (((CMap (kappa_1 R)) . (Y,Z)) + ((CMap (kappa_1 R)) . (Z,Y))) >= ((CMap (kappa_1 R)) . (X,Z)) + ((CMap (kappa_1 R)) . (Z,X)) ;
then ((delta_1 R) . (X,Y)) + (((CMap (kappa_1 R)) . (Y,Z)) + ((CMap (kappa_1 R)) . (Z,Y))) >= ((CMap (kappa_1 R)) . (X,Z)) + ((CMap (kappa_1 R)) . (Z,X)) by Delta1;
then ((delta_1 R) . (X,Y)) + ((delta_1 R) . (Y,Z)) >= ((CMap (kappa_1 R)) . (X,Z)) + ((CMap (kappa_1 R)) . (Z,X)) by Delta1;
hence ((delta_1 R) . (X,Y)) + ((delta_1 R) . (Y,Z)) >= (delta_1 R) . (X,Z) by Delta1; :: thesis: verum