defpred S1[ set ] means $1 is Subset of VAR;
A1: for x, y being Variable holds
( S1[H1(x,y)] & S1[H2(x,y)] )
proof
let x, y be Variable; :: thesis: ( S1[H1(x,y)] & S1[H2(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 ( S1[H1(x,y)] & S1[H2(x,y)] ) ; :: thesis: verum
end;
A2: for a, b being set st S1[a] & S1[b] holds
S1[H4(a,b)]
proof
let a, b be set ; :: thesis: ( S1[a] & S1[b] implies S1[H4(a,b)] )
assume A3: ( a is Subset of VAR & b is Subset of VAR ) ; :: thesis: S1[H4(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 S1[H4(a,b)] ; :: thesis: verum
end;
A6: for a being set
for x being Variable st S1[a] holds
S1[H5(x,a)] by XBOOLE_1:1;
A7: for a being set st S1[a] holds
S1[H3(a)] ;
thus S1[H6(H)] from ZF_MODEL:sch 4(Lm1, A1, A7, A2, A6); :: thesis: verum