let a, b be natural Ordinal; :: thesis: ( ( a <> {} or b <> {} ) implies ex c, d1, d2 being natural Ordinal st
( d1,d2 are_relative_prime & 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_relative_prime 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_relative_prime or not A = c *^ d1 or not B = c *^ d2 ) ) )
thus ( B c= A & A in omega & A <> {} ) by A1, A4, ORDINAL1:def 13; :: thesis: for c, d1, d2 being natural Ordinal holds
( not d1,d2 are_relative_prime or not A = c *^ d1 or not B = c *^ d2 )
thus for c, d1, d2 being natural Ordinal holds
( not d1,d2 are_relative_prime 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_relative_prime or not A = c *^ d1 or not B = c *^ d2 ) ) )
thus ( B c= A & A in omega & A <> {} ) by A1, A5, ORDINAL1:def 13; :: thesis: for c, d1, d2 being natural Ordinal holds
( not d1,d2 are_relative_prime or not A = c *^ d1 or not B = c *^ d2 )
thus for c, d1, d2 being natural Ordinal holds
( not d1,d2 are_relative_prime 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 & A in omega & A <> {} & ( for c, d1, d2 being natural Ordinal holds
( not d1,d2 are_relative_prime or not A = c *^ d1 or not B = c *^ d2 ) ) ) by A6;
reconsider A = A, B = B as Element of omega by A8, ORDINAL1:22;
( A = 1 *^ A & B = 1 *^ B ) by ORDINAL2:56;
then not A,B are_relative_prime by A8;
then consider c, d1, d2 being Ordinal such that
A9: ( A = c *^ d1 & B = c *^ d2 & c <> 1 ) by Def2;
A10: ( d1 <> {} & c <> {} ) by A8, A9, ORDINAL2:52, ORDINAL2:55;
then ( c c= A & d1 c= A & d2 c= B ) by A9, ORDINAL3:39;
then reconsider c = c, d1 = d1, d2 = d2 as Element of omega by ORDINAL1:22;
( A = d1 *^ c & B = d2 *^ c ) by A9;
then A11: d2 c= d1 by A8, A10, ORDINAL3:38;

B13: now

let c', d1', d2' be natural Ordinal; :: thesis: ( d1',d2' are_relative_prime & d1 = c' *^ d1' implies not d2 = c' *^ d2' )
assume A12: ( d1',d2' are_relative_prime & d1 = c' *^ d1' & d2 = c' *^ d2' ) ; :: thesis: contradiction
then ( A = (c *^ c') *^ d1' & B = (c *^ c') *^ d2' ) by A9, ORDINAL3:58;
hence contradiction by A8, A12; :: thesis: verum

end;

( 1 in c or c in 1 ) by A9, ORDINAL1:24;
then 1 *^ d1 in A by A9, A10, ORDINAL3:17, ORDINAL3:22;
then d1 in A by ORDINAL2:56;
hence contradiction by B13, A7, A10, A11, ORDINAL1:7; :: thesis: verum