let A, C1 be set ; :: thesis: ( A in F4() & C1 c= F4() & P1[C1] implies P1[C1 \/{A}] ) assume that A7:
A in F4()
and A8:
C1 c= F4()
and A9:
P1[C1]
; :: thesis: P1[C1 \/{A}] reconsider A9 = A as Cell of F3(),F2() byA7; reconsider C19 = C1 as Chain of F3(),F2() byA8, XBOOLE_1:1;