theorem Th2: :: GLIB_001:3

for X being set
for fs being FinSequence of X
for fss being Subset of fs holds len (Seq fss) <= len fs