let x, A be set ; :: thesis: ( x in B & A c= B & S₁[A] implies S₁[A \/ {x}] )
assume that
A4: x in B and
A5: A c= B and
A6: ( A <> {} implies ex B9 being Element of Fin F₁() st
( B9 = A & P₁[B9] ) ) and
A \/ {x} <> {} ; :: thesis: ex B9 being Element of Fin F₁() st
( B9 = A \/ {x} & P₁[B9] )
reconsider x9 = x as Element of F₁() by A4, Th6;
reconsider A9 = A as Element of Fin F₁() by A5, Th8;
take A9 \/ {.x9.} ; :: thesis: ( A9 \/ {.x9.} = A \/ {x} & P₁[A9 \/ {.x9.}] )
thus A9 \/ {.x9.} = A \/ {x} ; :: thesis: P₁[A9 \/ {.x9.}]
A7: P₁[{.x9.}] by A1;