let B be non empty Subset of F₁(); :: thesis: P₁[B]
reconsider BB = B as non empty Element of Fin F₁() by FINSUB_1:def 5;
defpred S₁[ Element of Fin F₁()] means ex C being Subset of F₁() st
( C = $1 & P₁[C] );
B1: for x being Element of F₁() holds S₁[{.x.}]

proof

let x be Element of F₁(); :: thesis: S₁[{.x.}]
P₁[{x}] by A1;
hence S₁[{.x.}] ; :: thesis: verum

end;

B2: for B1, B2 being non empty Element of Fin F₁() st S₁[B1] & S₁[B2] holds
S₁[B1 \/ B2]

proof

let B1, B2 be non empty Element of Fin F₁(); :: thesis: ( S₁[B1] & S₁[B2] implies S₁[B1 \/ B2] )
assume K1: ( S₁[B1] & S₁[B2] ) ; :: thesis: S₁[B1 \/ B2]
then reconsider A1 = B1, A2 = B2 as Subset of F₁() ;
P₁[A1 \/ A2] by A2, K1;
hence S₁[B1 \/ B2] ; :: thesis: verum

end;

for B being non empty Element of Fin F₁() holds S₁[B] from SETWISEO:sch 3(B1, B2);
then S₁[BB] ;
hence P₁[B] ; :: thesis: verum