theorem Th37: :: DIST_2:37

for S being non empty finite set
for X being Subset of S
for s being FinSequence of S holds s " X = trueEVENT ((MembershipDecision X) * s)