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