let X be set ; :: thesis: ( X is empty implies X is included_in_Seg )
assume A1: X is empty ; :: thesis: X is included_in_Seg
take 0 ; :: according to FINSEQ_1:def 13 :: thesis: X c= Seg 0
thus X c= Seg 0 by A1; :: thesis: verum