let R be finite Approximation_Space; :: thesis: for X, Y, Z being Subset of R holds ((CMap (kappa_2 R)) . (X,Y)) + ((CMap (kappa_2 R)) . (Y,Z)) >= (CMap (kappa_2 R)) . (X,Z)
let X, Y, Z be Subset of R; :: thesis: ((CMap (kappa_2 R)) . (X,Y)) + ((CMap (kappa_2 R)) . (Y,Z)) >= (CMap (kappa_2 R)) . (X,Z)
B1: (CMap (kappa_2 R)) . (X,Y) = (card (X \ Y)) / (card ([#] R)) by PropEx31;
B2: (CMap (kappa_2 R)) . (Y,Z) = (card (Y \ Z)) / (card ([#] R)) by PropEx31;
B3: (CMap (kappa_2 R)) . (X,Z) = (card (X \ Z)) / (card ([#] R)) by PropEx31;
A1: Y \ Z c= Y by XBOOLE_1:36;
X \ Y misses Y by XBOOLE_1:79;
then A2: card ((X \ Y) \/ (Y \ Z)) = (card (X \ Y)) + (card (Y \ Z)) by CARD_2:40, A1, XBOOLE_1:63;
X \ Z c= (X \ Y) \/ (Y \ Z)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X \ Z or x in (X \ Y) \/ (Y \ Z) )
assume x in X \ Z ; :: thesis: x in (X \ Y) \/ (Y \ Z)
then A3: ( x in X & not x in Z ) by XBOOLE_0:def 5;
per cases ( x in Y or not x in Y ) ;
suppose x in Y ; :: thesis: x in (X \ Y) \/ (Y \ Z)
then x in Y \ Z by A3, XBOOLE_0:def 5;
hence x in (X \ Y) \/ (Y \ Z) by XBOOLE_0:def 3; :: thesis: verum
end;
suppose not x in Y ; :: thesis: x in (X \ Y) \/ (Y \ Z)
then x in X \ Y by A3, XBOOLE_0:def 5;
hence x in (X \ Y) \/ (Y \ Z) by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
then ((card (X \ Y)) + (card (Y \ Z))) / (card ([#] R)) >= (card (X \ Z)) / (card ([#] R)) by A2, XREAL_1:72, NAT_1:43;
hence ((CMap (kappa_2 R)) . (X,Y)) + ((CMap (kappa_2 R)) . (Y,Z)) >= (CMap (kappa_2 R)) . (X,Z) by B1, B2, B3, XCMPLX_1:62; :: thesis: verum