defpred S1[ Element of F1(), Element of Fin F1()] means ex y being Element of F1() st
( y in $2 & P1[y,$1] & ( for z being Element of F1() st z in $2 & P1[z,y] holds
P1[y,z] ) );
defpred S2[ Element of Fin F1()] means for x being Element of F1() st x in $1 holds
S1[x,$1];
A3: now :: thesis: for B being Element of Fin F1()
for x being Element of F1() st S2[B] holds
S2[B \/ {.x.}]
let B be Element of Fin F1(); :: thesis: for x being Element of F1() st S2[B] holds
S2[B \/ {.x.}]
let x be Element of F1(); :: thesis: ( S2[B] implies S2[B \/ {.x.}] )
assume A4: S2[B] ; :: thesis: S2[B \/ {.x.}]
thus S2[B \/ {.x.}] :: thesis: verum
proof
let z be Element of F1(); :: thesis: ( z in B \/ {.x.} implies S1[z,B \/ {.x.}] )
assume A5: z in B \/ {x} ; :: thesis: S1[z,B \/ {.x.}]
now :: thesis: S1[z,B \/ {.x.}]
per cases ( z in B or z = x ) by A5, ZFMISC_1:136;
suppose z in B ; :: thesis: S1[z,B \/ {.x.}]
then consider y being Element of F1() such that
A6: y in B and
A7: P1[y,z] and
A8: for x being Element of F1() st x in B & P1[x,y] holds
P1[y,x] by A4;
now :: thesis: ( ( P1[x,y] & x in B \/ {x} & P1[x,z] & ( for v being Element of F1() st v in B \/ {x} & P1[v,x] holds
P1[x,v] ) ) or ( P1[x,y] & y in B \/ {x} & P1[y,z] & ( for v being Element of F1() st v in B \/ {x} & P1[v,y] holds
P1[y,v] ) ) )
per cases ( P1[x,y] or not P1[x,y] ) ;
case A9: P1[x,y] ; :: thesis: ( x in B \/ {x} & P1[x,z] & ( for v being Element of F1() st v in B \/ {x} & P1[v,x] holds
P1[x,v] ) )
thus x in B \/ {x} by ZFMISC_1:136; :: thesis: ( P1[x,z] & ( for v being Element of F1() st v in B \/ {x} & P1[v,x] holds
P1[x,v] ) )
thus P1[x,z] by A2, A7, A9; :: thesis: for v being Element of F1() st v in B \/ {x} & P1[v,x] holds
P1[x,v]
let v be Element of F1(); :: thesis: ( v in B \/ {x} & P1[v,x] implies P1[x,v] )
assume that
A10: v in B \/ {x} and
A11: P1[v,x] ; :: thesis: P1[x,v]
A12: now :: thesis: ( v in B implies P1[x,v] )
assume A13: v in B ; :: thesis: P1[x,v]
P1[v,y] by A2, A9, A11;
then P1[y,v] by A8, A13;
hence P1[x,v] by A2, A9; :: thesis: verum
end;
( v in B or v = x ) by A10, ZFMISC_1:136;
hence P1[x,v] by A1, A12; :: thesis: verum
end;
case A14: P1[x,y] ; :: thesis: ( y in B \/ {x} & P1[y,z] & ( for v being Element of F1() st v in B \/ {x} & P1[v,y] holds
P1[y,v] ) )
thus y in B \/ {x} by A6, XBOOLE_0:def 3; :: thesis: ( P1[y,z] & ( for v being Element of F1() st v in B \/ {x} & P1[v,y] holds
P1[y,v] ) )
thus P1[y,z] by A7; :: thesis: for v being Element of F1() st v in B \/ {x} & P1[v,y] holds
P1[y,v]
let v be Element of F1(); :: thesis: ( v in B \/ {x} & P1[v,y] implies P1[y,v] )
assume that
A15: v in B \/ {x} and
A16: P1[v,y] ; :: thesis: P1[y,v]
( v in B or v = x ) by A15, ZFMISC_1:136;
hence P1[y,v] by A8, A14, A16; :: thesis: verum
end;
end;
end;
hence S1[z,B \/ {.x.}] ; :: thesis: verum
end;
suppose A17: z = x ; :: thesis: S1[z,B \/ {.x.}]
now :: thesis: ( ( ex w being Element of F1() st
( w in B & P1[w,x] ) & ex u being Element of F1() st
( u in B \/ {x} & P1[u,z] & ( for v being Element of F1() st v in B \/ {x} & P1[v,u] holds
P1[u,v] ) ) ) or ( ( for w being Element of F1() st w in B holds
not P1[w,x] ) & x in B \/ {x} & P1[x,x] & ( for v being Element of F1() st v in B \/ {x} & P1[v,x] holds
P1[x,v] ) ) )
per cases ( ex w being Element of F1() st
( w in B & P1[w,x] ) or for w being Element of F1() st w in B holds
not P1[w,x] ) ;
case ex w being Element of F1() st
( w in B & P1[w,x] ) ; :: thesis: ex u being Element of F1() st
( u in B \/ {x} & P1[u,z] & ( for v being Element of F1() st v in B \/ {x} & P1[v,u] holds
P1[u,v] ) )
then consider w being Element of F1() such that
A18: w in B and
A19: P1[w,z] by A17;
consider y being Element of F1() such that
A20: y in B and
A21: P1[y,w] and
A22: for x being Element of F1() st x in B & P1[x,y] holds
P1[y,x] by A4, A18;
take u = y; :: thesis: ( u in B \/ {x} & P1[u,z] & ( for v being Element of F1() st v in B \/ {x} & P1[v,u] holds
P1[u,v] ) )
thus u in B \/ {x} by A20, XBOOLE_0:def 3; :: thesis: ( P1[u,z] & ( for v being Element of F1() st v in B \/ {x} & P1[v,u] holds
P1[u,v] ) )
thus P1[u,z] by A2, A19, A21; :: thesis: for v being Element of F1() st v in B \/ {x} & P1[v,u] holds
P1[u,v]
let v be Element of F1(); :: thesis: ( v in B \/ {x} & P1[v,u] implies P1[u,v] )
assume that
A23: v in B \/ {x} and
A24: P1[v,u] ; :: thesis: P1[u,v]
( v in B or v = x ) by A23, ZFMISC_1:136;
hence P1[u,v] by A2, A17, A19, A21, A22, A24; :: thesis: verum
end;
case A25: for w being Element of F1() st w in B holds
not P1[w,x] ; :: thesis: ( x in B \/ {x} & P1[x,x] & ( for v being Element of F1() st v in B \/ {x} & P1[v,x] holds
P1[x,v] ) )
thus x in B \/ {x} by ZFMISC_1:136; :: thesis: ( P1[x,x] & ( for v being Element of F1() st v in B \/ {x} & P1[v,x] holds
P1[x,v] ) )
thus A26: P1[x,x] by A1; :: thesis: for v being Element of F1() st v in B \/ {x} & P1[v,x] holds
P1[x,v]
let v be Element of F1(); :: thesis: ( v in B \/ {x} & P1[v,x] implies P1[x,v] )
assume that
A27: v in B \/ {x} and
A28: P1[v,x] ; :: thesis: P1[x,v]
not v in B by A25, A28;
hence P1[x,v] by A26, A27, ZFMISC_1:136; :: thesis: verum
end;
end;
end;
hence S1[z,B \/ {.x.}] by A17; :: thesis: verum
end;
end;
end;
hence S1[z,B \/ {.x.}] ; :: thesis: verum
end;
end;
A29: S2[ {}. F1()] ;
for B being Element of Fin F1() holds S2[B] from SETWISEO:sch 4(A29, A3);
 hence for x being Element of F1() st x in F2() holds
ex y being Element of F1() st
( y in F2() & P1[y,x] & ( for z being Element of F1() st z in F2() & P1[z,y] holds
P1[y,z] ) ) ; :: thesis: verum