let a, b be natural Ordinal; ( ( a <> {} or b <> {} ) implies ex c, d1, d2 being natural Ordinal st
( d1,d2 are_coprime & a = c *^ d1 & b = c *^ d2 ) )
assume that
A1:
( a <> {} or b <> {} )
and
A2:
for c, d1, d2 being natural Ordinal holds
( not d1,d2 are_coprime or not a = c *^ d1 or not b = c *^ d2 )
; contradiction
A3:
ex A being Ordinal st S1[A]
proof
per cases
( a c= b or b c= a )
;
suppose A4:
a c= b
;
ex A being Ordinal st S1[A]take A =
b;
S1[A]take B =
a;
( B c= A & A in omega & A <> {} & ( for c, d1, d2 being natural Ordinal holds
( not d1,d2 are_coprime or not A = c *^ d1 or not B = c *^ d2 ) ) )thus
(
B c= A &
A in omega &
A <> {} )
by A1, A4, ORDINAL1:def 12;
for c, d1, d2 being natural Ordinal holds
( not d1,d2 are_coprime or not A = c *^ d1 or not B = c *^ d2 )thus
for
c,
d1,
d2 being
natural Ordinal holds
( not
d1,
d2 are_coprime or not
A = c *^ d1 or not
B = c *^ d2 )
by A2;
verum end; suppose A5:
b c= a
;
ex A being Ordinal st S1[A]take A =
a;
S1[A]take B =
b;
( B c= A & A in omega & A <> {} & ( for c, d1, d2 being natural Ordinal holds
( not d1,d2 are_coprime or not A = c *^ d1 or not B = c *^ d2 ) ) )thus
(
B c= A &
A in omega &
A <> {} )
by A1, A5, ORDINAL1:def 12;
for c, d1, d2 being natural Ordinal holds
( not d1,d2 are_coprime or not A = c *^ d1 or not B = c *^ d2 )thus
for
c,
d1,
d2 being
natural Ordinal holds
( not
d1,
d2 are_coprime or not
A = c *^ d1 or not
B = c *^ d2 )
by A2;
verum end;
end;
consider A being Ordinal such that
A6:
S1[A]
and
A7:
for C being Ordinal st S1[C] holds
A c= C
from ORDINAL1:sch 1(A3);
consider B being Ordinal such that
A8:
B c= A
and
A9:
A in omega
and
A10:
A <> {}
and
A11:
for c, d1, d2 being natural Ordinal holds
( not d1,d2 are_coprime or not A = c *^ d1 or not B = c *^ d2 )
by A6;
reconsider A = A, B = B as Element of omega by A8, A9, ORDINAL1:12;
( A = 1 *^ A & B = 1 *^ B )
by ORDINAL2:39;
then
not A,B are_coprime
by A11;
then consider c, d1, d2 being Ordinal such that
A12:
A = c *^ d1
and
A13:
B = c *^ d2
and
A14:
c <> 1
;
A15:
c <> {}
by A10, A12, ORDINAL2:35;
then A16:
( d1 c= A & d2 c= B )
by A12, A13, ORDINAL3:36;
A17:
d1 <> {}
by A10, A12, ORDINAL2:38;
then
c c= A
by A12, ORDINAL3:36;
then reconsider c = c, d1 = d1, d2 = d2 as Element of omega by A16, ORDINAL1:12;
( 1 in c or c in 1 )
by A14, ORDINAL1:14;
then
1 *^ d1 in A
by A12, A17, A15, ORDINAL3:14, ORDINAL3:19;
then A18:
d1 in A
by ORDINAL2:39;
( A = d1 *^ c & B = d2 *^ c )
by A12, A13;
then
d2 c= d1
by A8, A15, ORDINAL3:35;
hence
contradiction
by A7, A17, A19, A18, ORDINAL1:5; verum