let R be finite Approximation_Space; :: thesis: for X, Y, Z being Subset of R holds ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,Z)) >= (CMap (kappa_1 R)) . (X,Z)
let X, Y, Z be Subset of R; :: thesis: ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,Z)) >= (CMap (kappa_1 R)) . (X,Z)

per cases ( X = {} or ( X <> {} & Y = {} & Z <> {} ) or ( X <> {} & Y <> {} & Z = {} ) or ( X <> {} & Y = {} & Z = {} ) or ( X <> {} & Y <> {} & Z <> {} ) ) ;

suppose F1: X = {} ; :: thesis: ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,Z)) >= (CMap (kappa_1 R)) . (X,Z)

then X c= Y ;
then F2: (CMap (kappa_1 R)) . (X,Y) = 0 by Prop6a;
(CMap (kappa_1 R)) . (X,Z) = 0 by Prop6a, F1, XBOOLE_1:2;
hence ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,Z)) >= (CMap (kappa_1 R)) . (X,Z) by F2, XXREAL_1:1; :: thesis: verum

end;

suppose F1: ( X <> {} & Y = {} & Z <> {} ) ; :: thesis: ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,Z)) >= (CMap (kappa_1 R)) . (X,Z)

then Y c= Z ;
then F2: (CMap (kappa_1 R)) . (Y,Z) = 0 by Prop6a;
(CMap (kappa_1 R)) . (X,Y) = 1 by F1, Ble1;
hence ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,Z)) >= (CMap (kappa_1 R)) . (X,Z) by F2, XXREAL_1:1; :: thesis: verum

end;

suppose F1: ( X <> {} & Y <> {} & Z = {} ) ; :: thesis: ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,Z)) >= (CMap (kappa_1 R)) . (X,Z)

then F3: (CMap (kappa_1 R)) . (X,Z) = 1 by Ble1;
(CMap (kappa_1 R)) . (X,Y) >= 0 by XXREAL_1:1;
then ((CMap (kappa_1 R)) . (X,Y)) + 1 >= 0 + 1 by XREAL_1:6;
hence ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,Z)) >= (CMap (kappa_1 R)) . (X,Z) by F1, F3, Ble1; :: thesis: verum

end;

suppose F1: ( X <> {} & Y = {} & Z = {} ) ; :: thesis: ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,Z)) >= (CMap (kappa_1 R)) . (X,Z)

then F3: (CMap (kappa_1 R)) . (X,Y) = 1 by Ble1;
(CMap (kappa_1 R)) . (Y,Z) >= 0 by XXREAL_1:1;
then 1 + ((CMap (kappa_1 R)) . (Y,Z)) >= 1 + 0 by XREAL_1:6;
hence ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,Z)) >= (CMap (kappa_1 R)) . (X,Z) by F1, F3; :: thesis: verum

end;

suppose ( X <> {} & Y <> {} & Z <> {} ) ; :: thesis: ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,Z)) >= (CMap (kappa_1 R)) . (X,Z)

hence ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,Z)) >= (CMap (kappa_1 R)) . (X,Z) by Jaga1; :: thesis: verum

end;

end;