theorem Th40: :: FINSEQ_3:42

for X, Y being set
for i, j being Nat st X c= Seg i & Y c= Seg j holds
( ( for m, n being Nat st m in X & n in Y holds
m < n ) iff Sgm (X \/ Y) = (Sgm X) ^ (Sgm Y) )