let RLS be non empty RLSStruct ; :: thesis: for A, B being Subset-Family of RLS holds |.(Complex_of (A \/ B)).| = |.(Complex_of A).| \/ |.(Complex_of B).|
let A, B be Subset-Family of RLS; :: thesis: |.(Complex_of (A \/ B)).| = |.(Complex_of A).| \/ |.(Complex_of B).|
set CA = Complex_of A;
set CB = Complex_of B;
set CAB = Complex_of (A \/ B);
A1: the topology of (Complex_of A) \/ the topology of (Complex_of B) = the topology of (Complex_of (A \/ B)) by SIMPLEX0:5;
thus |.(Complex_of (A \/ B)).| c= |.(Complex_of A).| \/ |.(Complex_of B).| :: according to XBOOLE_0:def 10 :: thesis: |.(Complex_of A).| \/ |.(Complex_of B).| c= |.(Complex_of (A \/ B)).|

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in |.(Complex_of (A \/ B)).| or x in |.(Complex_of A).| \/ |.(Complex_of B).| )
assume x in |.(Complex_of (A \/ B)).| ; :: thesis: x in |.(Complex_of A).| \/ |.(Complex_of B).|
then consider S being Subset of (Complex_of (A \/ B)) such that
A2: S is simplex-like and
A3: x in conv (@ S) by Def3;
A4: S in the topology of (Complex_of (A \/ B)) by A2;

per cases ( S in the topology of (Complex_of A) or S in the topology of (Complex_of B) ) by A1, A4, XBOOLE_0:def 3;

suppose A5: S in the topology of (Complex_of A) ; :: thesis: x in |.(Complex_of A).| \/ |.(Complex_of B).|

reconsider S1 = S as Subset of (Complex_of A) ;
( @ S = @ S1 & S1 is simplex-like ) by A5;
then conv (@ S) c= |.(Complex_of A).| by Th5;
hence x in |.(Complex_of A).| \/ |.(Complex_of B).| by A3, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A6: S in the topology of (Complex_of B) ; :: thesis: x in |.(Complex_of A).| \/ |.(Complex_of B).|

reconsider S1 = S as Subset of (Complex_of B) ;
( @ S = @ S1 & S1 is simplex-like ) by A6;
then conv (@ S) c= |.(Complex_of B).| by Th5;
hence x in |.(Complex_of A).| \/ |.(Complex_of B).| by A3, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

( |.(Complex_of A).| c= |.(Complex_of (A \/ B)).| & |.(Complex_of B).| c= |.(Complex_of (A \/ B)).| ) by A1, Th4, XBOOLE_1:7;
hence |.(Complex_of A).| \/ |.(Complex_of B).| c= |.(Complex_of (A \/ B)).| by XBOOLE_1:8; :: thesis: verum