defpred S_{1}[ Element of F_{1}(), Element of Fin F_{1}()] means ex y being Element of F_{1}() st

( y in $2 & P_{1}[y,$1] & ( for z being Element of F_{1}() st z in $2 & P_{1}[z,y] holds

P_{1}[y,z] ) );

defpred S_{2}[ Element of Fin F_{1}()] means for x being Element of F_{1}() st x in $1 holds

S_{1}[x,$1];

_{2}[ {}. F_{1}()]
;

for B being Element of Fin F_{1}() holds S_{2}[B]
from SETWISEO:sch 4(A29, A3);

hence for x being Element of F_{1}() st x in F_{2}() holds

ex y being Element of F_{1}() st

( y in F_{2}() & P_{1}[y,x] & ( for z being Element of F_{1}() st z in F_{2}() & P_{1}[z,y] holds

P_{1}[y,z] ) )
; :: thesis: verum

( y in $2 & P

P

defpred S

S

A3: now :: thesis: for B being Element of Fin F_{1}()

for x being Element of F_{1}() st S_{2}[B] holds

S_{2}[B \/ {.x.}]

A29:
Sfor x being Element of F

S

let B be Element of Fin F_{1}(); :: thesis: for x being Element of F_{1}() st S_{2}[B] holds

S_{2}[B \/ {.x.}]

let x be Element of F_{1}(); :: thesis: ( S_{2}[B] implies S_{2}[B \/ {.x.}] )

assume A4: S_{2}[B]
; :: thesis: S_{2}[B \/ {.x.}]

thus S_{2}[B \/ {.x.}]
:: thesis: verum

end;S

let x be Element of F

assume A4: S

thus S

proof

let z be Element of F_{1}(); :: thesis: ( z in B \/ {.x.} implies S_{1}[z,B \/ {.x.}] )

assume A5: z in B \/ {x} ; :: thesis: S_{1}[z,B \/ {.x.}]

_{1}[z,B \/ {.x.}]
; :: thesis: verum

end;assume A5: z in B \/ {x} ; :: thesis: S

now :: thesis: S_{1}[z,B \/ {.x.}]end;

hence
Sper cases
( z in B or z = x )
by A5, ZFMISC_1:136;

end;

suppose
z in B
; :: thesis: S_{1}[z,B \/ {.x.}]

then consider y being Element of F_{1}() such that

A6: y in B and

A7: P_{1}[y,z]
and

A8: for x being Element of F_{1}() st x in B & P_{1}[x,y] holds

P_{1}[y,x]
by A4;

_{1}[z,B \/ {.x.}]
; :: thesis: verum

end;A6: y in B and

A7: P

A8: for x being Element of F

P

now :: thesis: ( ( P_{1}[x,y] & x in B \/ {x} & P_{1}[x,z] & ( for v being Element of F_{1}() st v in B \/ {x} & P_{1}[v,x] holds

P_{1}[x,v] ) ) or ( P_{1}[x,y] & y in B \/ {x} & P_{1}[y,z] & ( for v being Element of F_{1}() st v in B \/ {x} & P_{1}[v,y] holds

P_{1}[y,v] ) ) )end;

hence
SP

P

per cases
( P_{1}[x,y] or not P_{1}[x,y] )
;

end;

case A9:
P_{1}[x,y]
; :: thesis: ( x in B \/ {x} & P_{1}[x,z] & ( for v being Element of F_{1}() st v in B \/ {x} & P_{1}[v,x] holds

P_{1}[x,v] ) )

P

thus
x in B \/ {x}
by ZFMISC_1:136; :: thesis: ( P_{1}[x,z] & ( for v being Element of F_{1}() st v in B \/ {x} & P_{1}[v,x] holds

P_{1}[x,v] ) )

thus P_{1}[x,z]
by A2, A7, A9; :: thesis: for v being Element of F_{1}() st v in B \/ {x} & P_{1}[v,x] holds

P_{1}[x,v]

let v be Element of F_{1}(); :: thesis: ( v in B \/ {x} & P_{1}[v,x] implies P_{1}[x,v] )

assume that

A10: v in B \/ {x} and

A11: P_{1}[v,x]
; :: thesis: P_{1}[x,v]

hence P_{1}[x,v]
by A1, A12; :: thesis: verum

end;P

thus P

P

let v be Element of F

assume that

A10: v in B \/ {x} and

A11: P

A12: now :: thesis: ( v in B implies P_{1}[x,v] )

( v in B or v = x )
by A10, ZFMISC_1:136;assume A13:
v in B
; :: thesis: P_{1}[x,v]

P_{1}[v,y]
by A2, A9, A11;

then P_{1}[y,v]
by A8, A13;

hence P_{1}[x,v]
by A2, A9; :: thesis: verum

end;P

then P

hence P

hence P

case A14:
P_{1}[x,y]
; :: thesis: ( y in B \/ {x} & P_{1}[y,z] & ( for v being Element of F_{1}() st v in B \/ {x} & P_{1}[v,y] holds

P_{1}[y,v] ) )

P

thus
y in B \/ {x}
by A6, XBOOLE_0:def 3; :: thesis: ( P_{1}[y,z] & ( for v being Element of F_{1}() st v in B \/ {x} & P_{1}[v,y] holds

P_{1}[y,v] ) )

thus P_{1}[y,z]
by A7; :: thesis: for v being Element of F_{1}() st v in B \/ {x} & P_{1}[v,y] holds

P_{1}[y,v]

let v be Element of F_{1}(); :: thesis: ( v in B \/ {x} & P_{1}[v,y] implies P_{1}[y,v] )

assume that

A15: v in B \/ {x} and

A16: P_{1}[v,y]
; :: thesis: P_{1}[y,v]

( v in B or v = x ) by A15, ZFMISC_1:136;

hence P_{1}[y,v]
by A8, A14, A16; :: thesis: verum

end;P

thus P

P

let v be Element of F

assume that

A15: v in B \/ {x} and

A16: P

( v in B or v = x ) by A15, ZFMISC_1:136;

hence P

suppose A17:
z = x
; :: thesis: S_{1}[z,B \/ {.x.}]

_{1}[z,B \/ {.x.}]
by A17; :: thesis: verum

end;

now :: thesis: ( ( ex w being Element of F_{1}() st

( w in B & P_{1}[w,x] ) & ex u being Element of F_{1}() st

( u in B \/ {x} & P_{1}[u,z] & ( for v being Element of F_{1}() st v in B \/ {x} & P_{1}[v,u] holds

P_{1}[u,v] ) ) ) or ( ( for w being Element of F_{1}() st w in B holds

not P_{1}[w,x] ) & x in B \/ {x} & P_{1}[x,x] & ( for v being Element of F_{1}() st v in B \/ {x} & P_{1}[v,x] holds

P_{1}[x,v] ) ) )end;

hence
S( w in B & P

( u in B \/ {x} & P

P

not P

P

per cases
( ex w being Element of F_{1}() st

( w in B & P_{1}[w,x] ) or for w being Element of F_{1}() st w in B holds

not P_{1}[w,x] )
;

end;

( w in B & P

not P

case
ex w being Element of F_{1}() st

( w in B & P_{1}[w,x] )
; :: thesis: ex u being Element of F_{1}() st

( u in B \/ {x} & P_{1}[u,z] & ( for v being Element of F_{1}() st v in B \/ {x} & P_{1}[v,u] holds

P_{1}[u,v] ) )

( w in B & P

( u in B \/ {x} & P

P

then consider w being Element of F_{1}() such that

A18: w in B and

A19: P_{1}[w,z]
by A17;

consider y being Element of F_{1}() such that

A20: y in B and

A21: P_{1}[y,w]
and

A22: for x being Element of F_{1}() st x in B & P_{1}[x,y] holds

P_{1}[y,x]
by A4, A18;

take u = y; :: thesis: ( u in B \/ {x} & P_{1}[u,z] & ( for v being Element of F_{1}() st v in B \/ {x} & P_{1}[v,u] holds

P_{1}[u,v] ) )

thus u in B \/ {x} by A20, XBOOLE_0:def 3; :: thesis: ( P_{1}[u,z] & ( for v being Element of F_{1}() st v in B \/ {x} & P_{1}[v,u] holds

P_{1}[u,v] ) )

thus P_{1}[u,z]
by A2, A19, A21; :: thesis: for v being Element of F_{1}() st v in B \/ {x} & P_{1}[v,u] holds

P_{1}[u,v]

let v be Element of F_{1}(); :: thesis: ( v in B \/ {x} & P_{1}[v,u] implies P_{1}[u,v] )

assume that

A23: v in B \/ {x} and

A24: P_{1}[v,u]
; :: thesis: P_{1}[u,v]

( v in B or v = x ) by A23, ZFMISC_1:136;

hence P_{1}[u,v]
by A2, A17, A19, A21, A22, A24; :: thesis: verum

end;A18: w in B and

A19: P

consider y being Element of F

A20: y in B and

A21: P

A22: for x being Element of F

P

take u = y; :: thesis: ( u in B \/ {x} & P

P

thus u in B \/ {x} by A20, XBOOLE_0:def 3; :: thesis: ( P

P

thus P

P

let v be Element of F

assume that

A23: v in B \/ {x} and

A24: P

( v in B or v = x ) by A23, ZFMISC_1:136;

hence P

case A25:
for w being Element of F_{1}() st w in B holds

not P_{1}[w,x]
; :: thesis: ( x in B \/ {x} & P_{1}[x,x] & ( for v being Element of F_{1}() st v in B \/ {x} & P_{1}[v,x] holds

P_{1}[x,v] ) )

not P

P

thus
x in B \/ {x}
by ZFMISC_1:136; :: thesis: ( P_{1}[x,x] & ( for v being Element of F_{1}() st v in B \/ {x} & P_{1}[v,x] holds

P_{1}[x,v] ) )

thus A26: P_{1}[x,x]
by A1; :: thesis: for v being Element of F_{1}() st v in B \/ {x} & P_{1}[v,x] holds

P_{1}[x,v]

let v be Element of F_{1}(); :: thesis: ( v in B \/ {x} & P_{1}[v,x] implies P_{1}[x,v] )

assume that

A27: v in B \/ {x} and

A28: P_{1}[v,x]
; :: thesis: P_{1}[x,v]

not v in B by A25, A28;

hence P_{1}[x,v]
by A26, A27, ZFMISC_1:136; :: thesis: verum

end;P

thus A26: P

P

let v be Element of F

assume that

A27: v in B \/ {x} and

A28: P

not v in B by A25, A28;

hence P

for B being Element of Fin F

hence for x being Element of F

ex y being Element of F

( y in F

P