theorem :: ZF_LANG1:114

for p, q being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= (p 'or' q) => (q 'or' p) & M |= (p 'or' q) => (q 'or' p) )