let B be non empty Subset of F1(); :: thesis: P1[B]
reconsider BB = B as non empty Element of Fin F1() by FINSUB_1:def 5;
defpred S1[ Element of Fin F1()] means ex C being Subset of F1() st
( C = $1 & P1[C] );
B1: for x being Element of F1() holds S1[{.x.}]
proof
let x be Element of F1(); :: thesis: S1[{.x.}]
P1[{x}] by A1;
hence S1[{.x.}] ; :: thesis: verum
end;
B2: for B1, B2 being non empty Element of Fin F1() st S1[B1] & S1[B2] holds
S1[B1 \/ B2]
proof
let B1, B2 be non empty Element of Fin F1(); :: thesis: ( S1[B1] & S1[B2] implies S1[B1 \/ B2] )
assume K1: ( S1[B1] & S1[B2] ) ; :: thesis: S1[B1 \/ B2]
then reconsider A1 = B1, A2 = B2 as Subset of F1() ;
P1[A1 \/ A2] by A2, K1;
hence S1[B1 \/ B2] ; :: thesis: verum
end;
for B being non empty Element of Fin F1() holds S1[B] from SETWISEO:sch 3(B1, B2);
 then S1[BB] ;
hence P1[B] ; :: thesis: verum