theorem Th3: :: MMLQUERY:3

for X being set
for L being List of X
for x being Element of X
for O being Operation of X holds
( x in L WHERE O iff ( x in L & x . O <> {} ) )