deffunc H₁( set ) -> set = { x where x is Element of F₁() : $1 c= x } ;
given x being set such that A3: x in F₁() and
A4: P₁[x] ; :: thesis: contradiction
defpred S₁[ Nat] means ex s being Element of F₁() st
( card H₁(s) = $1 & P₁[s] );
H₁(x) c= F₁()

proof

let x1 be object ; :: according to TARSKI:def 3 :: thesis: ( not x1 in H₁(x) or x1 in F₁() )
assume x1 in H₁(x) ; :: thesis: x1 in F₁()
then ex xx being Element of F₁() st
( x1 = xx & x c= xx ) ;
hence x1 in F₁() ; :: thesis: verum

end;

then reconsider Ux = H₁(x) as finite set ;
A5: ex k being Nat st S₁[k]

proof

reconsider x = x as Element of F₁() by A3;
take k = card Ux; :: thesis: S₁[k]
take x ; :: thesis: ( card H₁(x) = k & P₁[x] )
thus card H₁(x) = k ; :: thesis: P₁[x]
thus P₁[x] by A4; :: thesis: verum

end;

consider k being Nat such that
A6: S₁[k] and
A7: for n being Nat st S₁[n] holds
k <= n from NAT_1:sch 5(A5);
consider s being Element of F₁() such that
A8: card H₁(s) = k and
A9: P₁[s] by A6;

per cases ( s is_/\-irreducible_in F₁() or s is_/\-reducible_in F₁() ) ;

suppose s is_/\-irreducible_in F₁() ; :: thesis: contradiction

hence contradiction by A1, A9; :: thesis: verum

end;

suppose A10: s is_/\-reducible_in F₁() ; :: thesis: contradiction

H₁(s) c= F₁()

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H₁(s) or x in F₁() )
assume x in H₁(s) ; :: thesis: x in F₁()
then ex xx being Element of F₁() st
( x = xx & s c= xx ) ;
hence x in F₁() ; :: thesis: verum

end;

then reconsider Us = H₁(s) as finite set ;
consider z, y being set such that
A11: z in F₁() and
A12: y in F₁() and
A13: s = z /\ y and
A14: s <> z and
A15: s <> y by A10;
A16: s c= y by A13, XBOOLE_1:17;
H₁(z) c= F₁()

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H₁(z) or x in F₁() )
assume x in H₁(z) ; :: thesis: x in F₁()
then ex xx being Element of F₁() st
( x = xx & z c= xx ) ;
hence x in F₁() ; :: thesis: verum

end;

then reconsider Uz = H₁(z) as finite set ;
H₁(y) c= F₁()

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H₁(y) or x in F₁() )
assume x in H₁(y) ; :: thesis: x in F₁()
then ex xx being Element of F₁() st
( x = xx & y c= xx ) ;
hence x in F₁() ; :: thesis: verum

end;

then reconsider Uy = H₁(y) as finite set ;
A17: s c= z by A13, XBOOLE_1:17;
reconsider y = y, z = z as Element of F₁() by A11, A12;
A18: Uy c= Us

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Uy or x in Us )
assume x in Uy ; :: thesis: x in Us
then consider xx being Element of F₁() such that
A19: x = xx and
A20: y c= xx ;
s c= xx by A16, A20;
hence x in Us by A19; :: thesis: verum

end;

now :: thesis: not s in Uy

assume s in Uy ; :: thesis: contradiction
then ex x being Element of F₁() st
( s = x & y c= x ) ;
hence contradiction by A15, A16, XBOOLE_0:def 10; :: thesis: verum

end;

then Uy <> Us ;
then Uy c< Us by A18, XBOOLE_0:def 8;
then card Us > card Uy by TREES_1:6;
then A21: P₁[y] by A7, A8;
A22: Uz c= Us

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Uz or x in Us )
assume x in Uz ; :: thesis: x in Us
then consider xx being Element of F₁() such that
A23: x = xx and
A24: z c= xx ;
s c= xx by A17, A24;
hence x in Us by A23; :: thesis: verum

end;

now :: thesis: not s in Uz

assume s in Uz ; :: thesis: contradiction
then ex x being Element of F₁() st
( s = x & z c= x ) ;
hence contradiction by A14, A17, XBOOLE_0:def 10; :: thesis: verum

end;

then Uz <> Us ;
then Uz c< Us by A22, XBOOLE_0:def 8;
then card Us > card Uz by TREES_1:6;
then P₁[z] by A7, A8;
hence contradiction by A2, A9, A13, A21; :: thesis: verum

end;

end;