theorem Th4: :: GLIB_001:5

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