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);
x. 0 in Free (All (x. 2),(((x. 2) 'in' (x. 0 )) => ((x. 2) 'in' (x. 1))))

proof

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:67
.= ((Free ((x. 2) 'in' (x. 0 ))) \/ (Free ((x. 2) 'in' (x. 1)))) \ {(x. 2)} by ZF_LANG1:69
.= ((Free ((x. 2) 'in' (x. 0 ))) \/ {(x. 2),(x. 1)}) \ {(x. 2)} by ZF_LANG1:64
.= ({(x. 2),(x. 0 )} \/ {(x. 2),(x. 1)}) \ {(x. 2)} by ZF_LANG1:64
.= ({(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:23, ZF_LANG1:86
.= {(x. 0 )} \/ {(x. 1)} by ZFMISC_1:23, ZF_LANG1:86
.= {(x. 0 ),(x. 1)} by ENUMSET1:41 ;
hence x. 0 in Free (All (x. 2),(((x. 2) 'in' (x. 0 )) => ((x. 2) 'in' (x. 1)))) by TARSKI:def 2; :: thesis: verum

end;

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 set ; :: 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 & E,(f / (x. 1),e) / (x. 0 ),m |= All (x. 2),(((x. 2) 'in' (x. 0 )) => ((x. 2) 'in' (x. 1))) ) by A1;
A4: m c= E by A2;
m c= e

proof

let u1 be set ; :: according to TARSKI:def 3 :: thesis: ( not u1 in m or u1 in e )
assume A5: u1 in m ; :: thesis: u1 in e
then reconsider u1 = u1 as Element of E by A4;
( x. 0 <> x. 2 & x. 0 <> x. 1 & x. 1 <> x. 2 ) by ZF_LANG1:86;
then A6: ( (((f / (x. 1),e) / (x. 0 ),m) / (x. 2),u1) . (x. 2) = u1 & m = ((f / (x. 1),e) / (x. 0 ),m) . (x. 0 ) & (((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) & (f / (x. 1),e) . (x. 1) = e & (((f / (x. 1),e) / (x. 0 ),m) / (x. 2),u1) . (x. 0 ) = ((f / (x. 1),e) / (x. 0 ),m) . (x. 0 ) ) by FUNCT_7:34, FUNCT_7:130;
then ( E,((f / (x. 1),e) / (x. 0 ),m) / (x. 2),u1 |= (x. 2) 'in' (x. 0 ) & E,((f / (x. 1),e) / (x. 0 ),m) / (x. 2),u1 |= ((x. 2) 'in' (x. 0 )) => ((x. 2) 'in' (x. 1)) ) by A3, A5, ZF_LANG1:80, ZF_MODEL:13;
then E,((f / (x. 1),e) / (x. 0 ),m) / (x. 2),u1 |= (x. 2) 'in' (x. 1) by ZF_MODEL:18;
hence u1 in e by A6, ZF_MODEL:13; :: thesis: verum

end;

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

end;

let u be set ; :: 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 A7: 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 A8: ( u in E & u in bool e ) by XBOOLE_0:def 4;
reconsider u = u as Element of E by A7, XBOOLE_0:def 4;

now

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))
( x. 0 <> x. 2 & x. 0 <> x. 1 & x. 1 <> x. 2 ) by ZF_LANG1:86;
then A9: ( (((f / (x. 1),e) / (x. 0 ),u) / (x. 2),m) . (x. 2) = m & u = ((f / (x. 1),e) / (x. 0 ),u) . (x. 0 ) & (((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) & (f / (x. 1),e) . (x. 1) = e & (((f / (x. 1),e) / (x. 0 ),u) / (x. 2),m) . (x. 0 ) = ((f / (x. 1),e) / (x. 0 ),u) . (x. 0 ) ) by FUNCT_7:34, FUNCT_7:130;

now

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 A9, ZF_MODEL:13;
hence E,((f / (x. 1),e) / (x. 0 ),u) / (x. 2),m |= (x. 2) 'in' (x. 1) by A8, A9, 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:80;
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