theorem Th61: :: FOMODEL0:61

for A, B, Y, X being set st A is_finer_than B & X is_finer_than Y holds
A \/ X is_finer_than B \/ Y