let W be Universe; :: thesis: for Y being Subclass of W st Y is closed_wrt_A1-A7 & Y is epsilon-transitive holds
Y is predicatively_closed
let Y be Subclass of W; :: thesis: ( Y is closed_wrt_A1-A7 & Y is epsilon-transitive implies Y is predicatively_closed )
assume that
A1: Y is closed_wrt_A1-A7 and
A2: Y is epsilon-transitive ; :: thesis: Y is predicatively_closed
let H be ZF-formula; :: according to ZF_FUND2:def 2 :: thesis: for E being non empty set
for f being Function of VAR,E st E in Y holds
Section (H,f) in Y
let E be non empty set ; :: thesis: for f being Function of VAR,E st E in Y holds
Section (H,f) in Y
let f be Function of VAR,E; :: thesis: ( E in Y implies Section (H,f) in Y )
assume A3: E in Y ; :: thesis: Section (H,f) in Y

now :: thesis: Section (H,f) in Y

per cases ( not x. 0 in Free H or x. 0 in Free H ) ;

suppose not x. 0 in Free H ; :: thesis: Section (H,f) in Y

then Section (H,f) = {} by Def1;
hence Section (H,f) in Y by A1, ZF_FUND1:3; :: thesis: verum

end;

suppose A4: x. 0 in Free H ; :: thesis: Section (H,f) in Y

reconsider a = E as Element of W by A3;
reconsider n = {} as Element of omega by ORDINAL1:def 11;
set fs = (code (Free H)) \ {n};
A5: Diagram (H,E) in Y by A1, A3, ZF_FUND1:22;
then reconsider b = Diagram (H,E) as Element of W ;
A6: b c= Funcs ((((code (Free H)) \ {n}) \/ {n}),a)

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in b or u in Funcs ((((code (Free H)) \ {n}) \/ {n}),a) )
assume u in b ; :: thesis: u in Funcs ((((code (Free H)) \ {n}) \/ {n}),a)
then ex f1 being Function of VAR,E st
( u = (f1 * decode) | (code (Free H)) & f1 in St (H,E) ) by ZF_FUND1:def 5;
then A7: u in Funcs ((code (Free H)),a) by ZF_FUND1:31;
x". (x. 0) in code (Free H) by A4, ZF_FUND1:33;
then n in code (Free H) by ZF_FUND1:def 3;
then {n} c= code (Free H) by ZFMISC_1:31;
hence u in Funcs ((((code (Free H)) \ {n}) \/ {n}),a) by A7, XBOOLE_1:45; :: thesis: verum

end;

n in {n} by TARSKI:def 1;
then A8: not n in (code (Free H)) \ {n} by XBOOLE_0:def 5;
A9: (f * decode) | ((code (Free H)) \ {n}) in Funcs (((code (Free H)) \ {n}),a) by ZF_FUND1:31;
Funcs (((code (Free H)) \ {n}),a) in Y by A1, A3, ZF_FUND1:9;
then reconsider y = (f * decode) | ((code (Free H)) \ {n}) as Element of W by A9, ZF_FUND1:1;
set B = { e where e is Element of E : {[n,e]} \/ y in b } ;
set A = { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } ;
A10: { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } = { e where e is Element of E : {[n,e]} \/ y in b }

proof

thus { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } c= { e where e is Element of E : {[n,e]} \/ y in b } :: according to XBOOLE_0:def 10 :: thesis: { e where e is Element of E : {[n,e]} \/ y in b } c= { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) }

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } or u in { e where e is Element of E : {[n,e]} \/ y in b } )
assume u in { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } ; :: thesis: u in { e where e is Element of E : {[n,e]} \/ y in b }
then ex w being Element of W st
( u = w & w in a & {[n,w]} \/ y in b ) ;
hence u in { e where e is Element of E : {[n,e]} \/ y in b } ; :: thesis: verum

end;

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in { e where e is Element of E : {[n,e]} \/ y in b } or u in { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } )
assume u in { e where e is Element of E : {[n,e]} \/ y in b } ; :: thesis: u in { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) }
then consider e being Element of E such that
A11: u = e and
A12: {[n,e]} \/ y in b ;
reconsider e = e as Element of W by A3, ZF_FUND1:1;
e in { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } by A12;
hence u in { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } by A11; :: thesis: verum

end;

a c= Y by A2, A3;
then { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } in Y by A1, A3, A5, A9, A8, A6, ZF_FUND1:16;
hence Section (H,f) in Y by A10, Th4; :: thesis: verum

end;

end;

end;

hence Section (H,f) in Y ; :: thesis: verum