let a, b be natural Ordinal; :: thesis: ( ( 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 ) ; :: thesis: contradiction
A3: ex A being Ordinal st S₁[A]

proof

per cases ( a c= b or b c= a ) ;

suppose A4: a c= b ; :: thesis: ex A being Ordinal st S₁[A]

take A = b; :: thesis: S₁[A]
take B = a; :: thesis: ( 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; :: thesis: 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; :: thesis: verum

end;

suppose A5: b c= a ; :: thesis: ex A being Ordinal st S₁[A]

take A = a; :: thesis: S₁[A]
take B = b; :: thesis: ( 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; :: thesis: 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; :: thesis: verum

end;

end;

end;

consider A being Ordinal such that
A6: S₁[A] and
A7: for C being Ordinal st S₁[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;

A19: now :: thesis: for c9, d19, d29 being natural Ordinal st d19,d29 are_coprime & d1 = c9 *^ d19 holds
not d2 = c9 *^ d29

let c9, d19, d29 be natural Ordinal; :: thesis: ( d19,d29 are_coprime & d1 = c9 *^ d19 implies not d2 = c9 *^ d29 )
assume that
A20: d19,d29 are_coprime and
A21: ( d1 = c9 *^ d19 & d2 = c9 *^ d29 ) ; :: thesis: contradiction
( A = (c *^ c9) *^ d19 & B = (c *^ c9) *^ d29 ) by A12, A13, A21, ORDINAL3:50;
hence contradiction by A11, A20; :: thesis: verum

end;

( 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; :: thesis: verum