for FT being non empty RelStr
for A, B, C being Subset of FT st A,B are_separated & A,C are_separated holds
A,B \/ C are_separated