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

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

let v be Function of VAR,M; :: thesis: M,v |= (p <=> q) => (p => q)
( M,v |= p <=> q implies M,v |= p => q ) by ZF_MODEL:15;
hence M,v |= (p <=> q) => (p => q) by ZF_MODEL:18; :: thesis: verum

end;

hence M,v |= (p <=> q) => (p => q) ; :: thesis: M |= (p <=> q) => (p => q)
let v be Function of VAR,M; :: according to ZF_MODEL:def 5 :: thesis: M,v |= (p <=> q) => (p => q)
thus M,v |= (p <=> q) => (p => q) by A1; :: thesis: verum