theorem Th5: :: ZF_MODEL:5

for E being non empty set
for H, H9 being ZF-formula
for f being Function of VAR,E holds
( ( f in St (H,E) & f in St (H9,E) ) iff f in St ((H '&' H9),E) )