let R be finite Approximation_Space; :: thesis: for X, Y, Z being Subset of R st X <> {} & Y <> {} & Z <> {} 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: ( X <> {} & Y <> {} & Z <> {} implies ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,Z)) >= (CMap (kappa_1 R)) . (X,Z) )
assume ZZ: ( X <> {} & Y <> {} & Z <> {} ) ; :: thesis: ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,Z)) >= (CMap (kappa_1 R)) . (X,Z)
set m = card ((X \/ Y) \/ Z);
set m0 = card (X \ (Y \/ Z));
set m1 = card (Y \ (X \/ Z));
set m2 = card ((X /\ Y) \ Z);
set m3 = card ((X /\ Z) \ Y);
set m4 = card (Z \ (X \/ Y));
D1: X \ (Y \/ Z) = (X \ Y) /\ (X \ Z) by XBOOLE_1:53;
X /\ Z misses X \ Z by XBOOLE_1:89;
then (X /\ Z) \ Y misses X \ Z by XBOOLE_1:80;
then D3b: (card (X \ (Y \/ Z))) + (card ((X /\ Z) \ Y)) = card ((X \ (Y \/ Z)) \/ ((X /\ Z) \ Y)) by CARD_2:40, D1, XBOOLE_1:74;
Y = (Y \ Z) \/ Y by XBOOLE_1:12, XBOOLE_1:36
.= ((Y \/ Z) \ Z) \/ Y by XBOOLE_1:40
.= ((Y \/ Z) \ Z) \/ ((Y \/ Z) /\ Y) by XBOOLE_1:21
.= (Y \/ Z) \ (Z \ Y) by XBOOLE_1:52 ;
then u1: (X \ (Y \/ Z)) \/ (X /\ (Z \ Y)) = X \ Y by XBOOLE_1:52;
X \ (Y \/ Z) misses X /\ Y by D1, XBOOLE_1:74, XBOOLE_1:89;
then D2: X \ (Y \/ Z) misses (X /\ Y) \ Z by XBOOLE_1:63, XBOOLE_1:36;
D3: (card (X \ (Y \/ Z))) + (card ((X /\ Y) \ Z)) = card ((X \ (Y \/ Z)) \/ ((X /\ Y) \ Z)) by D2, CARD_2:40;
Z = (Z \ Y) \/ Z by XBOOLE_1:12, XBOOLE_1:36
.= ((Y \/ Z) \ Y) \/ Z by XBOOLE_1:40
.= ((Y \/ Z) \ Y) \/ ((Y \/ Z) /\ Z) by XBOOLE_1:21
.= (Y \/ Z) \ (Y \ Z) by XBOOLE_1:52 ;
then (X \ (Y \/ Z)) \/ (X /\ (Y \ Z)) = X \ Z by XBOOLE_1:52;
then Z2: card (X \ Z) = (card (X \ (Y \/ Z))) + (card ((X /\ Y) \ Z)) by D3, XBOOLE_1:49;
d1: Y \ (X \/ Z) c= Y \ X by XBOOLE_1:34, XBOOLE_1:7;
X /\ Y misses Y \ X by XBOOLE_1:89;
then Y \ (X \/ Z) misses X /\ Y by d1, XBOOLE_1:63;
then D2: Y \ (X \/ Z) misses (X /\ Y) \ Z by XBOOLE_1:63, XBOOLE_1:36;
D3a: (card (Y \ (X \/ Z))) + (card ((X /\ Y) \ Z)) = card ((Y \ (X \/ Z)) \/ ((X /\ Y) \ Z)) by D2, CARD_2:40;
Z = (Z \ X) \/ Z by XBOOLE_1:12, XBOOLE_1:36
.= ((X \/ Z) \ X) \/ Z by XBOOLE_1:40
.= ((X \/ Z) \ X) \/ ((X \/ Z) /\ Z) by XBOOLE_1:21
.= (X \/ Z) \ (X \ Z) by XBOOLE_1:52 ;
then aa: (Y \ (X \/ Z)) \/ (Y /\ (X \ Z)) = Y \ Z by XBOOLE_1:52;
then Z3: card (Y \ Z) = (card (Y \ (X \/ Z))) + (card ((X /\ Y) \ Z)) by D3a, XBOOLE_1:49;
(Z \ (X \/ Y)) \/ (X \/ Y) = (X \/ Y) \/ Z by XBOOLE_1:39;
then x4: (card (Z \ (X \/ Y))) + (card (X \/ Y)) = card ((X \/ Y) \/ Z) by XBOOLE_1:79, CARD_2:40;
(Y \ (X \/ Z)) \/ (X \/ Z) = Y \/ (X \/ Z) by XBOOLE_1:39
.= (X \/ Y) \/ Z by XBOOLE_1:4 ;
then z5: (card (Y \ (X \/ Z))) + (card (X \/ Z)) = card ((X \/ Y) \/ Z) by XBOOLE_1:79, CARD_2:40;
then card (X \/ Z) = (card ((X \/ Y) \/ Z)) - (card (Y \ (X \/ Z))) ;
then U3: card ((X \/ Y) \/ Z) > 0 + (card (Y \ (X \/ Z))) by XREAL_1:20, ZZ;
(X \ (Y \/ Z)) \/ (Y \/ Z) = X \/ (Y \/ Z) by XBOOLE_1:39
.= (X \/ Y) \/ Z by XBOOLE_1:4 ;
then Z6: (card (X \ (Y \/ Z))) + (card (Y \/ Z)) = card ((X \/ Y) \/ Z) by XBOOLE_1:79, CARD_2:40;
T1: (CMap (kappa_1 R)) . (X,Y) = (card (X \ Y)) / (card (X \/ Y)) by ZZ, PropEx3
.= ((card (X \ (Y \/ Z))) + (card ((X /\ Z) \ Y))) / ((card ((X \/ Y) \/ Z)) - (card (Z \ (X \/ Y)))) by u1, x4, XBOOLE_1:49, D3b ;
T2: (CMap (kappa_1 R)) . (Y,Z) = (card (Y \ Z)) / (card (Y \/ Z)) by ZZ, PropEx3
.= ((card (Y \ (X \/ Z))) + (card ((X /\ Y) \ Z))) / ((card ((X \/ Y) \/ Z)) - (card (X \ (Y \/ Z)))) by aa, Z6, XBOOLE_1:49, D3a ;
T3: (CMap (kappa_1 R)) . (X,Z) = ((card (X \ (Y \/ Z))) + (card ((X /\ Y) \ Z))) / ((card ((X \/ Y) \/ Z)) - (card (Y \ (X \/ Z)))) by Z2, z5, ZZ, PropEx3;
0 <= card (Z \ (X \/ Y)) ;
then (card ((X \/ Y) \/ Z)) - (card ((X \/ Y) \/ Z)) <= card (Z \ (X \/ Y)) ;
then (card ((X \/ Y) \/ Z)) - (card (Z \ (X \/ Y))) <= card ((X \/ Y) \/ Z) by XREAL_1:12;
then V1: ((card (X \ (Y \/ Z))) + (card ((X /\ Z) \ Y))) / ((card ((X \/ Y) \/ Z)) - (card (Z \ (X \/ Y)))) >= ((card (X \ (Y \/ Z))) + (card ((X /\ Z) \ Y))) / (card ((X \/ Y) \/ Z)) by XREAL_1:118, x4, ZZ;
0 <= card (X \ (Y \/ Z)) ;
then (card ((X \/ Y) \/ Z)) - (card ((X \/ Y) \/ Z)) <= card (X \ (Y \/ Z)) ;
then (card ((X \/ Y) \/ Z)) - (card (X \ (Y \/ Z))) <= card ((X \/ Y) \/ Z) by XREAL_1:12;
then V2: ((card (Y \ (X \/ Z))) + (card ((X /\ Y) \ Z))) / ((card ((X \/ Y) \/ Z)) - (card (X \ (Y \/ Z)))) >= ((card (Y \ (X \/ Z))) + (card ((X /\ Y) \ Z))) / (card ((X \/ Y) \/ Z)) by XREAL_1:118, Z6, ZZ;
(card (X \ (Y \/ Z))) + (card ((X /\ Z) \ Y)) >= (card (X \ (Y \/ Z))) + 0 by XREAL_1:6;
then V3: ((card (X \ (Y \/ Z))) + (card ((X /\ Z) \ Y))) + ((card (Y \ (X \/ Z))) + (card ((X /\ Y) \ Z))) >= ((card (X \ (Y \/ Z))) + 0) + ((card (Y \ (X \/ Z))) + (card ((X /\ Y) \ Z))) by XREAL_1:6;
B2: (((card (X \ (Y \/ Z))) + (card ((X /\ Z) \ Y))) / ((card ((X \/ Y) \/ Z)) - (card (Z \ (X \/ Y))))) + (((card (Y \ (X \/ Z))) + (card ((X /\ Y) \ Z))) / ((card ((X \/ Y) \/ Z)) - (card (X \ (Y \/ Z))))) >= (((card (X \ (Y \/ Z))) + (card ((X /\ Z) \ Y))) / (card ((X \/ Y) \/ Z))) + (((card (Y \ (X \/ Z))) + (card ((X /\ Y) \ Z))) / (card ((X \/ Y) \/ Z))) by V1, V2, XREAL_1:7;
(((card (X \ (Y \/ Z))) + (card ((X /\ Z) \ Y))) / (card ((X \/ Y) \/ Z))) + (((card (Y \ (X \/ Z))) + (card ((X /\ Y) \ Z))) / (card ((X \/ Y) \/ Z))) = (((card (X \ (Y \/ Z))) + (card ((X /\ Z) \ Y))) + ((card (Y \ (X \/ Z))) + (card ((X /\ Y) \ Z)))) / (card ((X \/ Y) \/ Z)) by XCMPLX_1:62;
then B3: (((card (X \ (Y \/ Z))) + (card ((X /\ Z) \ Y))) / (card ((X \/ Y) \/ Z))) + (((card (Y \ (X \/ Z))) + (card ((X /\ Y) \ Z))) / (card ((X \/ Y) \/ Z))) >= (((card (X \ (Y \/ Z))) + (card (Y \ (X \/ Z)))) + (card ((X /\ Y) \ Z))) / (card ((X \/ Y) \/ Z)) by V3, XREAL_1:72;
set a = ((card (X \ (Y \/ Z))) + (card (Y \ (X \/ Z)))) + (card ((X /\ Y) \ Z));
set b = card ((X \/ Y) \/ Z);
F2: ((card (X \ (Y \/ Z))) + (card (Y \ (X \/ Z)))) + (card ((X /\ Y) \ Z)) = (card (X \ (Y \/ Z))) + (card (Y \ Z)) by Z3;
X \ Y misses Y by XBOOLE_1:79;
then X \ Y misses Y \ Z by XBOOLE_1:63, XBOOLE_1:36;
then (X \ Y) /\ (X \ Z) misses Y \ Z by XBOOLE_1:74;
then F5: X \ (Y \/ Z) misses Y \ Z by XBOOLE_1:53;
( X \ (Y \/ Z) c= X & Y \ Z c= Y ) by XBOOLE_1:36;
then F4: (X \ (Y \/ Z)) \/ (Y \ Z) c= X \/ Y by XBOOLE_1:13;
X \/ Y c= (X \/ Y) \/ Z by XBOOLE_1:7;
then f6: (X \ (Y \/ Z)) \/ (Y \ Z) c= (X \/ Y) \/ Z by F4;
card ((X \ (Y \/ Z)) \/ (Y \ Z)) = ((card (X \ (Y \/ Z))) + (card (Y \ (X \/ Z)))) + (card ((X /\ Y) \ Z)) by F2, F5, CARD_2:40;
then (((card (X \ (Y \/ Z))) + (card (Y \ (X \/ Z)))) + (card ((X /\ Y) \ Z))) / (card ((X \/ Y) \/ Z)) >= ((((card (X \ (Y \/ Z))) + (card (Y \ (X \/ Z)))) + (card ((X /\ Y) \ Z))) - (card (Y \ (X \/ Z)))) / ((card ((X \/ Y) \/ Z)) - (card (Y \ (X \/ Z)))) by f6, U3, LemacikX, NAT_1:43;
then (((card (X \ (Y \/ Z))) + (card ((X /\ Z) \ Y))) / (card ((X \/ Y) \/ Z))) + (((card (Y \ (X \/ Z))) + (card ((X /\ Y) \ Z))) / (card ((X \/ Y) \/ Z))) >= ((card (X \ (Y \/ Z))) + (card ((X /\ Y) \ Z))) / ((card ((X \/ Y) \/ Z)) - (card (Y \ (X \/ Z)))) by B3, XXREAL_0:2;
hence ((CMap (kappa_1 R)) . (X,Y)) + ((CMap (kappa_1 R)) . (Y,Z)) >= (CMap (kappa_1 R)) . (X,Z) by T1, T2, T3, B2, XXREAL_0:2; :: thesis: verum