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;
( S1[H1(x,y)] & S1[H2(x,y)] )
{x,y} c= VAR
hence
(
S1[
H1(
x,
y)] &
S1[
H2(
x,
y)] )
;
verum
end;
A2:
for a, b being set st S1[a] & S1[b] holds
S1[H4(a,b)]
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); verum