theorem :: ZF_LANG1:5

for p, q being ZF-formula holds
( the_left_argument_of (p 'or' q) = p & the_right_argument_of (p 'or' q) = q )