theorem :: FINSEQ_1:51

for X being set st X is included_in_Seg holds
( Sgm X = {} iff X = {} )