theorem Th15: :: ZF_MODEL:15

for E being non empty set
for f being Function of VAR,E
for H, H9 being ZF-formula holds
( E,f |= H '&' H9 iff ( E,f |= H & E,f |= H9 ) ) by Th5;