defpred S₁[ set ] means $1 is Subset of VAR;
A1: for x, y being Variable holds
( S₁[H₁(x,y)] & S₁[H₂(x,y)] )

proof

let x, y be Variable; :: thesis: ( S₁[H₁(x,y)] & S₁[H₂(x,y)] )
{x,y} c= VAR

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {x,y} or a in VAR )
assume a in {x,y} ; :: thesis: a in VAR
then ( a = x or a = y ) by TARSKI:def 2;
hence a in VAR ; :: thesis: verum

end;

hence ( S₁[H₁(x,y)] & S₁[H₂(x,y)] ) ; :: thesis: verum

end;

A2: for a, b being set st S₁[a] & S₁[b] holds
S₁[H₄(a,b)]

proof

let a, b be set ; :: thesis: ( S₁[a] & S₁[b] implies S₁[H₄(a,b)] )
assume A3: ( a is Subset of VAR & b is Subset of VAR ) ; :: thesis: S₁[H₄(a,b)]
union {a,b} c= VAR

proof

let c be object ; :: according to TARSKI:def 3 :: thesis: ( not c in union {a,b} or c in VAR )
assume c in union {a,b} ; :: thesis: c in VAR
then consider X being set such that
A4: c in X and
A5: X in {a,b} by TARSKI:def 4;
X is Subset of VAR by A3, A5, TARSKI:def 2;
hence c in VAR by A4; :: thesis: verum

end;

hence S₁[H₄(a,b)] ; :: thesis: verum

end;

A6: for a being set
for x being Variable st S₁[a] holds
S₁[H₅(x,a)] by XBOOLE_1:1;
A7: for a being set st S₁[a] holds
S₁[H₃(a)] ;
thus S₁[H₆(H)] from ZF_MODEL:sch 4(Lm1, A1, A7, A2, A6); :: thesis: verum