theorem Th16: :: ZF_LANG:16

for F, G being ZF-formula holds (F '&' G) . 1 = 3