let p, q be ZF-formula; :: thesis: 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) )
let M be non empty set ; :: thesis: for v being Function of VAR,M holds
( M,v |= (p 'or' q) => (q 'or' p) & M |= (p 'or' q) => (q 'or' p) )
let v be Function of VAR,M; :: thesis: ( M,v |= (p 'or' q) => (q 'or' p) & M |= (p 'or' q) => (q 'or' p) )

now :: thesis: for v being Function of VAR,M holds M,v |= (p 'or' q) => (q 'or' p)

let v be Function of VAR,M; :: thesis: M,v |= (p 'or' q) => (q 'or' p)
A1: ( ( M,v |= p or M,v |= q ) implies M,v |= q 'or' p ) by ZF_MODEL:17;
( not M,v |= p 'or' q or M,v |= p or M,v |= q ) by ZF_MODEL:17;
hence M,v |= (p 'or' q) => (q 'or' p) by A1, ZF_MODEL:18; :: thesis: verum

end;

hence ( M,v |= (p 'or' q) => (q 'or' p) & M |= (p 'or' q) => (q 'or' p) ) ; :: thesis: verum