let B be non empty Subset of F_{1}(); :: thesis: P_{1}[B]

reconsider BB = B as non empty Element of Fin F_{1}() by FINSUB_1:def 5;

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

( C = $1 & P_{1}[C] );

B1: for x being Element of F_{1}() holds S_{1}[{.x.}]
_{1}() st S_{1}[B1] & S_{1}[B2] holds

S_{1}[B1 \/ B2]
_{1}() holds S_{1}[B]
from SETWISEO:sch 3(B1, B2);

then S_{1}[BB]
;

hence P_{1}[B]
; :: thesis: verum

reconsider BB = B as non empty Element of Fin F

defpred S

( C = $1 & P

B1: for x being Element of F

proof

B2:
for B1, B2 being non empty Element of Fin F
let x be Element of F_{1}(); :: thesis: S_{1}[{.x.}]

P_{1}[{x}]
by A1;

hence S_{1}[{.x.}]
; :: thesis: verum

end;P

hence S

S

proof

for B being non empty Element of Fin F
let B1, B2 be non empty Element of Fin F_{1}(); :: thesis: ( S_{1}[B1] & S_{1}[B2] implies S_{1}[B1 \/ B2] )

assume K1: ( S_{1}[B1] & S_{1}[B2] )
; :: thesis: S_{1}[B1 \/ B2]

then reconsider A1 = B1, A2 = B2 as Subset of F_{1}() ;

P_{1}[A1 \/ A2]
by A2, K1;

hence S_{1}[B1 \/ B2]
; :: thesis: verum

end;assume K1: ( S

then reconsider A1 = B1, A2 = B2 as Subset of F

P

hence S

then S

hence P