theorem :: MMLQUER2:21

for X being set
for S1, S2 being finite Subset of X
for R being connected Order of X holds
( order ((S1 \/ S2),R) = (order (S1,R)) ^ (order (S2,R)) iff for x, y being set st x in S1 & y in S2 holds
( x <> y & x,y in R ) )