:: deftheorem defines conjunctive ZF_LANG:def 13 :
for H being ZF-formula holds
( H is conjunctive iff ex F, G being ZF-formula st H = F '&' G );