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)).|

hence |.(Complex_of A).| \/ |.(Complex_of B).| c= |.(Complex_of (A \/ B)).| by XBOOLE_1:8; :: thesis: verum

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

( |.(Complex_of A).| c= |.(Complex_of (A \/ B)).| & |.(Complex_of B).| c= |.(Complex_of (A \/ B)).| )
by A1, Th4, XBOOLE_1:7;
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;

end;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;

end;

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;( @ 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

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;( @ 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

hence |.(Complex_of A).| \/ |.(Complex_of B).| c= |.(Complex_of (A \/ B)).| by XBOOLE_1:8; :: thesis: verum