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]
; contradiction
defpred S1[ Nat] means ex s being Element of F1() st
( card H1(s) = $1 & P1[s] );
H1(x) c= F1()
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;
S1[k]
take
x
;
( card H1(x) = k & P1[x] )
thus
card H1(
x)
= k
;
P1[x]
thus
P1[
x]
by A4;
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 A10:
s is_/\-reducible_in F1()
;
contradiction
H1(
s)
c= F1()
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()
then reconsider Uz =
H1(
z) as
finite set ;
H1(
y)
c= F1()
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
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
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;
verum end; end;