theorem Th52: :: PROB_3:52

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