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: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 ;
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 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 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 set ; :: 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:130;
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:80;
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:34, ZF_LANG1:86;
( 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:34, FUNCT_7:130, ZF_LANG1:86;
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:130, 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 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 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

A12: (f / (x. 1),e) . (x. 1) = e by FUNCT_7:130;
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:130;
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:34, FUNCT_7:130, ZF_LANG1:86;
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:34, ZF_LANG1:86;

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 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: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