theorem Th3: :: ZF_MODEL:3

for E being non empty set
for x, y being Variable
for f being Function of VAR,E holds
( f . x in f . y iff f in St ((x 'in' y),E) )