theorem Th40: :: FINSEQ_3:42

for X, Y being set st X is included_in_Seg & Y is included_in_Seg holds
( ( for m, n being Nat st m in X & n in Y holds
m < n ) iff Sgm (X \/ Y) = (Sgm X) ^ (Sgm Y) )