deffunc H1( set ) -> set = { x where x is Element of F1() : $1 c= x } ;
given x being set such that A3: x in F1() and
A4: P1[x] ; :: thesis: contradiction
defpred S1[ Nat] means ex s being Element of F1() st
( card H1(s) = $1 & P1[s] );
H1(x) c= F1()
proof
let x1 be object ; :: according to TARSKI:def 3 :: thesis: ( not x1 in H1(x) or x1 in F1() )
assume x1 in H1(x) ; :: thesis: x1 in F1()
then ex xx being Element of F1() st
( x1 = xx & x c= xx ) ;
hence x1 in F1() ; :: thesis: verum
end;
then reconsider Ux = H1(x) as finite set ;
A5: ex k being Nat st S1[k]
proof
reconsider x = x as Element of F1() by A3;
take k = card Ux; :: thesis: S1[k]
take x ; :: thesis: ( card H1(x) = k & P1[x] )
thus card H1(x) = k ; :: thesis: P1[x]
thus P1[x] by A4; :: thesis: verum
end;
consider k being Nat such that
A6: S1[k] and
A7: for n being Nat st S1[n] holds
k <= n from NAT_1:sch 5(A5);
 consider s being Element of F1() such that
A8: card H1(s) = k and
A9: P1[s] by A6;
per cases ( s is_/\-irreducible_in F1() or s is_/\-reducible_in F1() ) ;
suppose s is_/\-irreducible_in F1() ; :: thesis: contradiction
hence contradiction by A1, A9; :: thesis: verum
end;
suppose A10: s is_/\-reducible_in F1() ; :: thesis: contradiction
H1(s) c= F1()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H1(s) or x in F1() )
assume x in H1(s) ; :: thesis: x in F1()
then ex xx being Element of F1() st
( x = xx & s c= xx ) ;
hence x in F1() ; :: thesis: verum
end;
then reconsider Us = H1(s) as finite set ;
consider z, y being set such that
A11: z in F1() and
A12: y in F1() and
A13: s = z /\ y and
A14: s <> z and
A15: s <> y by A10;
A16: s c= y by A13, XBOOLE_1:17;
H1(z) c= F1()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H1(z) or x in F1() )
assume x in H1(z) ; :: thesis: x in F1()
then ex xx being Element of F1() st
( x = xx & z c= xx ) ;
hence x in F1() ; :: thesis: verum
end;
then reconsider Uz = H1(z) as finite set ;
H1(y) c= F1()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H1(y) or x in F1() )
assume x in H1(y) ; :: thesis: x in F1()
then ex xx being Element of F1() st
( x = xx & y c= xx ) ;
hence x in F1() ; :: thesis: verum
end;
then reconsider Uy = H1(y) as finite set ;
A17: s c= z by A13, XBOOLE_1:17;
reconsider y = y, z = z as Element of F1() 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 F1() 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 F1() 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: P1[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 F1() 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 F1() 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 P1[z] by A7, A8;
hence contradiction by A2, A9, A13, A21; :: thesis: verum
end;
end;