theorem Th51: :: PROB_3:51

for X being set
for F1 being FinSequence of bool X
for x being object st F1 <> {} holds
( x in Intersection F1 iff for k being Nat st k in dom F1 holds
x in F1 . k )