theorem th1: :: FIELD_5:8

for X being set holds
not for o being object holds o in X