theorem :: SIMPLEX1:9

for RLS being non empty RLSStruct
for A, B being Subset-Family of RLS holds |.(Complex_of (A \/ B)).| = |.(Complex_of A).| \/ |.(Complex_of B).|