let RLS be non empty RLSStruct ; :: thesis: for A, B being Subset-Family of RLS holds |.(Complex_of (A \/ B)).| = |.().| \/ |.().|
let A, B be Subset-Family of RLS; :: thesis: |.(Complex_of (A \/ B)).| = |.().| \/ |.().|
set CA = Complex_of A;
set CB = Complex_of B;
set CAB = Complex_of (A \/ B);
A1: the topology of () \/ the topology of () = the topology of (Complex_of (A \/ B)) by SIMPLEX0:5;
thus |.(Complex_of (A \/ B)).| c= |.().| \/ |.().| :: according to XBOOLE_0:def 10 :: thesis: |.().| \/ |.().| 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 |.().| \/ |.().| )
assume x in |.(Complex_of (A \/ B)).| ; :: thesis: x in |.().| \/ |.().|
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 () or S in the topology of () ) by ;
suppose A5: S in the topology of () ; :: thesis: x in |.().| \/ |.().|
reconsider S1 = S as Subset of () ;
( @ S = @ S1 & S1 is simplex-like ) by A5;
then conv (@ S) c= |.().| by Th5;
hence x in |.().| \/ |.().| by ; :: thesis: verum
end;
suppose A6: S in the topology of () ; :: thesis: x in |.().| \/ |.().|
reconsider S1 = S as Subset of () ;
( @ S = @ S1 & S1 is simplex-like ) by A6;
then conv (@ S) c= |.().| by Th5;
hence x in |.().| \/ |.().| by ; :: thesis: verum
end;
end;
end;
( |.().| c= |.(Complex_of (A \/ B)).| & |.().| c= |.(Complex_of (A \/ B)).| ) by ;
hence |.().| \/ |.().| c= |.(Complex_of (A \/ B)).| by XBOOLE_1:8; :: thesis: verum