for R being RelStr
for X, Y being well_founded Subset of R st X is lower holds
X \/ Y is well_founded Subset of R