theorem Th2: :: FINTOPO3:2

for T being non empty RelStr
for A being Subset of T
for x being Element of T holds
( x in A ^d iff for y being Element of T st y in A ` holds
not x in U_FT y )