set IR = the InternalRel of R;
set CR = the carrier of R;
set FIR = FinOrd R;
set FCR = Fin the carrier of R;
A1: FinPoset R = RelStr(# (Fin the carrier of R),() #) ;
now :: thesis: for x, y being Element of () holds
( x <= y or y <= x )
let x, y be Element of (); :: thesis: ( x <= y or y <= x )
reconsider x9 = x, y9 = y as Element of Fin the carrier of R ;
defpred S1[ Nat] means for x, y being Element of Fin the carrier of R holds
( not card x = R or [x,y] in FinOrd R or [y,x] in FinOrd R );
now :: thesis: for a, b being Element of Fin the carrier of R holds
( not card a = 0 or [a,b] in FinOrd R or [a,b] in FinOrd R )
let a, b be Element of Fin the carrier of R; :: thesis: ( not card a = 0 or [a,b] in FinOrd R or [a,b] in FinOrd R )
assume card a = 0 ; :: thesis: ( [a,b] in FinOrd R or [a,b] in FinOrd R )
then a = {} ;
hence ( [a,b] in FinOrd R or [a,b] in FinOrd R ) by ; :: thesis: verum
end;
then A2: S1[ 0 ] ;
now :: thesis: for n being Nat st ( for x, y being Element of Fin the carrier of R holds
( not card x = n or [x,y] in FinOrd R or [y,x] in FinOrd R ) ) holds
for a, b being Element of Fin the carrier of R holds
( not card a = n + 1 or [a,b] in FinOrd R or [b,a] in FinOrd R )
let n be Nat; :: thesis: ( ( for x, y being Element of Fin the carrier of R holds
( not card x = n or [x,y] in FinOrd R or [y,x] in FinOrd R ) ) implies for a, b being Element of Fin the carrier of R holds
( not card a = n + 1 or [b4,b5] in FinOrd R or [b5,b4] in FinOrd R ) )

assume A3: for x, y being Element of Fin the carrier of R holds
( not card x = n or [x,y] in FinOrd R or [y,x] in FinOrd R ) ; :: thesis: for a, b being Element of Fin the carrier of R holds
( not card a = n + 1 or [b4,b5] in FinOrd R or [b5,b4] in FinOrd R )

let a, b be Element of Fin the carrier of R; :: thesis: ( not card a = n + 1 or [b2,b3] in FinOrd R or [b3,b2] in FinOrd R )
assume A4: card a = n + 1 ; :: thesis: ( [b2,b3] in FinOrd R or [b3,b2] in FinOrd R )
per cases ( a = {} or a <> {} ) ;
suppose a = {} ; :: thesis: ( [b2,b3] in FinOrd R or [b3,b2] in FinOrd R )
hence ( [a,b] in FinOrd R or [b,a] in FinOrd R ) by ; :: thesis: verum
end;
suppose A5: a <> {} ; :: thesis: ( [b2,b3] in FinOrd R or [b3,b2] in FinOrd R )
now :: thesis: ( [a,b] in FinOrd R or [b,a] in FinOrd R )
per cases ( b = {} or b <> {} ) ;
suppose b = {} ; :: thesis: ( [a,b] in FinOrd R or [b,a] in FinOrd R )
hence ( [a,b] in FinOrd R or [b,a] in FinOrd R ) by ; :: thesis: verum
end;
suppose A6: b <> {} ; :: thesis: ( [a,b] in FinOrd R or [b,a] in FinOrd R )
now :: thesis: ( [a,b] in FinOrd R or [b,a] in FinOrd R )
per cases ;
suppose A7: PosetMax a <> PosetMax b ; :: thesis: ( [a,b] in FinOrd R or [b,a] in FinOrd R )
now :: thesis: ( [a,b] in FinOrd R or [b,a] in FinOrd R )
per cases by WAYBEL_0:def 29;
suppose PosetMax a <= PosetMax b ; :: thesis: ( [a,b] in FinOrd R or [b,a] in FinOrd R )
then [(),()] in the InternalRel of R by ORDERS_2:def 5;
hence ( [a,b] in FinOrd R or [b,a] in FinOrd R ) by A1, A5, A6, A7, Th36; :: thesis: verum
end;
suppose PosetMax b <= PosetMax a ; :: thesis: ( [a,b] in FinOrd R or [b,a] in FinOrd R )
then [(),()] in the InternalRel of R by ORDERS_2:def 5;
hence ( [a,b] in FinOrd R or [b,a] in FinOrd R ) by A1, A5, A6, A7, Th36; :: thesis: verum
end;
end;
end;
hence ( [a,b] in FinOrd R or [b,a] in FinOrd R ) ; :: thesis: verum
end;
suppose A8: PosetMax a = PosetMax b ; :: thesis: ( [a,b] in FinOrd R or [b,a] in FinOrd R )
set ax = a \ {()};
set bx = b \ {()};
A9: card (a \ {()}) = n by ;
reconsider ax = a \ {()}, bx = b \ {()} as Element of Fin the carrier of R by Th34;
now :: thesis: ( [a,b] in FinOrd R or [b,a] in FinOrd R )
per cases ( [ax,bx] in FinOrd R or [bx,ax] in FinOrd R ) by A3, A9;
suppose [ax,bx] in FinOrd R ; :: thesis: ( [a,b] in FinOrd R or [b,a] in FinOrd R )
hence ( [a,b] in FinOrd R or [b,a] in FinOrd R ) by A1, A5, A6, A8, Th36; :: thesis: verum
end;
suppose [bx,ax] in FinOrd R ; :: thesis: ( [a,b] in FinOrd R or [b,a] in FinOrd R )
hence ( [a,b] in FinOrd R or [b,a] in FinOrd R ) by A1, A5, A6, A8, Th36; :: thesis: verum
end;
end;
end;
hence ( [a,b] in FinOrd R or [b,a] in FinOrd R ) ; :: thesis: verum
end;
end;
end;
hence ( [a,b] in FinOrd R or [b,a] in FinOrd R ) ; :: thesis: verum
end;
end;
end;
hence ( [a,b] in FinOrd R or [b,a] in FinOrd R ) ; :: thesis: verum
end;
end;
end;
then A10: for n being Nat st S1[n] holds
S1[n + 1] ;
A11: for n being Nat holds S1[n] from NAT_1:sch 2(A2, A10);
card x9 = card x ;
then ( [x9,y9] in FinOrd R or [y9,x9] in FinOrd R ) by A11;
hence ( x <= y or y <= x ) by ORDERS_2:def 5; :: thesis: verum
end;
hence FinPoset R is connected by WAYBEL_0:def 29; :: thesis: verum