let E be non empty set ; :: thesis: for e being Element of E
for f being Function of VAR,E st E is epsilon-transitive holds
Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) = E /\ (bool e)
let e be Element of E; :: thesis: for f being Function of VAR,E st E is epsilon-transitive holds
Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) = E /\ (bool e)
let f be Function of VAR,E; :: thesis: ( E is epsilon-transitive implies Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) = E /\ (bool e) )
set H = All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))));
set v = f / ((x. 1),e);
set S = Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e)));
Free (All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))) = (Free (((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1)))) \ {(x. 2)} by ZF_LANG1:62
.= ((Free ((x. 2) 'in' (x. 0))) \/ (Free ((x. 2) 'in' (x. 1)))) \ {(x. 2)} by ZF_LANG1:64
.= ((Free ((x. 2) 'in' (x. 0))) \/ {(x. 2),(x. 1)}) \ {(x. 2)} by ZF_LANG1:59
.= ({(x. 2),(x. 0)} \/ {(x. 2),(x. 1)}) \ {(x. 2)} by ZF_LANG1:59
.= ({(x. 2),(x. 0)} \ {(x. 2)}) \/ ({(x. 2),(x. 1)} \ {(x. 2)}) by XBOOLE_1:42
.= ({(x. 2),(x. 0)} \ {(x. 2)}) \/ {(x. 1)} by ZFMISC_1:17, ZF_LANG1:76
.= {(x. 0)} \/ {(x. 1)} by ZFMISC_1:17, ZF_LANG1:76
.= {(x. 0),(x. 1)} by ENUMSET1:1 ;
then x. 0 in Free (All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))) by TARSKI:def 2;
then A1: Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) = { m where m is Element of E : E,(f / ((x. 1),e)) / ((x. 0),m) |= All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1)))) } by Def1;
assume A2: for X being set st X in E holds
X c= E ; :: according to ORDINAL1:def 2 :: thesis: Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) = E /\ (bool e)
thus Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) c= E /\ (bool e) :: according to XBOOLE_0:def 10 :: thesis: E /\ (bool e) c= Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e)))

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) or u in E /\ (bool e) )
assume u in Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) ; :: thesis: u in E /\ (bool e)
then consider m being Element of E such that
A3: u = m and
A4: E,(f / ((x. 1),e)) / ((x. 0),m) |= All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1)))) by A1;
A5: m c= E by A2;
m c= e

proof

let u1 be object ; :: according to TARSKI:def 3 :: thesis: ( not u1 in m or u1 in e )
assume A6: u1 in m ; :: thesis: u1 in e
then reconsider u1 = u1 as Element of E by A5;
A7: (((f / ((x. 1),e)) / ((x. 0),m)) / ((x. 2),u1)) . (x. 2) = u1 by FUNCT_7:128;
A8: E,((f / ((x. 1),e)) / ((x. 0),m)) / ((x. 2),u1) |= ((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1)) by A4, ZF_LANG1:71;
A9: ( (((f / ((x. 1),e)) / ((x. 0),m)) / ((x. 2),u1)) . (x. 1) = ((f / ((x. 1),e)) / ((x. 0),m)) . (x. 1) & (f / ((x. 1),e)) . (x. 1) = ((f / ((x. 1),e)) / ((x. 0),m)) . (x. 1) ) by FUNCT_7:32, ZF_LANG1:76;
( m = ((f / ((x. 1),e)) / ((x. 0),m)) . (x. 0) & (((f / ((x. 1),e)) / ((x. 0),m)) / ((x. 2),u1)) . (x. 0) = ((f / ((x. 1),e)) / ((x. 0),m)) . (x. 0) ) by FUNCT_7:32, FUNCT_7:128, ZF_LANG1:76;
then E,((f / ((x. 1),e)) / ((x. 0),m)) / ((x. 2),u1) |= (x. 2) 'in' (x. 0) by A6, A7, ZF_MODEL:13;
then ( (f / ((x. 1),e)) . (x. 1) = e & E,((f / ((x. 1),e)) / ((x. 0),m)) / ((x. 2),u1) |= (x. 2) 'in' (x. 1) ) by A8, FUNCT_7:128, ZF_MODEL:18;
hence u1 in e by A7, A9, ZF_MODEL:13; :: thesis: verum

end;

then u in bool e by A3, ZFMISC_1:def 1;
hence u in E /\ (bool e) by A3, XBOOLE_0:def 4; :: thesis: verum

end;

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in E /\ (bool e) or u in Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) )
assume A10: u in E /\ (bool e) ; :: thesis: u in Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e)))
then A11: u in bool e by XBOOLE_0:def 4;
reconsider u = u as Element of E by A10, XBOOLE_0:def 4;

now :: thesis: for m being Element of E holds E,((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m) |= ((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))

A12: (f / ((x. 1),e)) . (x. 1) = e by FUNCT_7:128;
let m be Element of E; :: thesis: E,((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m) |= ((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))
A13: (((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m)) . (x. 2) = m by FUNCT_7:128;
A14: ( u = ((f / ((x. 1),e)) / ((x. 0),u)) . (x. 0) & (((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m)) . (x. 0) = ((f / ((x. 1),e)) / ((x. 0),u)) . (x. 0) ) by FUNCT_7:32, FUNCT_7:128, ZF_LANG1:76;
A15: ( (((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m)) . (x. 1) = ((f / ((x. 1),e)) / ((x. 0),u)) . (x. 1) & (f / ((x. 1),e)) . (x. 1) = ((f / ((x. 1),e)) / ((x. 0),u)) . (x. 1) ) by FUNCT_7:32, ZF_LANG1:76;

now :: thesis: ( E,((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m) |= (x. 2) 'in' (x. 0) implies E,((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m) |= (x. 2) 'in' (x. 1) )

assume E,((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m) |= (x. 2) 'in' (x. 0) ; :: thesis: E,((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m) |= (x. 2) 'in' (x. 1)
then m in u by A13, A14, ZF_MODEL:13;
hence E,((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m) |= (x. 2) 'in' (x. 1) by A11, A13, A15, A12, ZF_MODEL:13; :: thesis: verum

end;

hence E,((f / ((x. 1),e)) / ((x. 0),u)) / ((x. 2),m) |= ((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1)) by ZF_MODEL:18; :: thesis: verum

end;

then E,(f / ((x. 1),e)) / ((x. 0),u) |= All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1)))) by ZF_LANG1:71;
hence u in Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) by A1; :: thesis: verum