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),(FinOrd R) #) ;

now

let x, y be Element of (FinPoset R); :: thesis: ( x <= y or y <= x )
reconsider x' = x, y' = y as Element of Fin the carrier of R ;
defpred S₁[ Element of 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

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 A2: card a = 0 ; :: thesis: ( [a,b] in FinOrd R or [a,b] in FinOrd R )
a = {} by A2;
hence ( [a,b] in FinOrd R or [a,b] in FinOrd R ) by A1, Th40; :: thesis: verum

end;

then A3: S₁[ 0 ] ;

now

let n be Element of 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 [b₄,b₅] in FinOrd R or [b₅,b₄] in FinOrd R ) )
assume A4: 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 [b₄,b₅] in FinOrd R or [b₅,b₄] in FinOrd R )
let a, b be Element of Fin the carrier of R; :: thesis: ( not card a = n + 1 or [b₂,b₃] in FinOrd R or [b₃,b₂] in FinOrd R )
assume A5: card a = n + 1 ; :: thesis: ( [b₂,b₃] in FinOrd R or [b₃,b₂] in FinOrd R )

per cases ( a = {} or a <> {} ) ;

suppose a = {} ; :: thesis: ( [b₂,b₃] in FinOrd R or [b₃,b₂] in FinOrd R )

hence ( [a,b] in FinOrd R or [b,a] in FinOrd R ) by A1, Th40; :: thesis: verum

end;

suppose A6: a <> {} ; :: thesis: ( [b₂,b₃] in FinOrd R or [b₃,b₂] in FinOrd R )

now

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 A1, Th40; :: thesis: verum

end;

suppose A7: b <> {} ; :: thesis: ( [a,b] in FinOrd R or [b,a] in FinOrd R )

now

per cases ( PosetMax a <> PosetMax b or PosetMax a = PosetMax b ) ;

suppose A8: PosetMax a <> PosetMax b ; :: thesis: ( [a,b] in FinOrd R or [b,a] in FinOrd R )

now

per cases ( PosetMax a <= PosetMax b or PosetMax b <= PosetMax a ) by WAYBEL_0:def 29;

suppose PosetMax a <= PosetMax b ; :: thesis: ( [a,b] in FinOrd R or [b,a] in FinOrd R )

then [(PosetMax a),(PosetMax b)] in the InternalRel of R by ORDERS_2:def 9;
hence ( [a,b] in FinOrd R or [b,a] in FinOrd R ) by A1, A6, A7, A8, Th40; :: thesis: verum

end;

suppose PosetMax b <= PosetMax a ; :: thesis: ( [a,b] in FinOrd R or [b,a] in FinOrd R )

then [(PosetMax b),(PosetMax a)] in the InternalRel of R by ORDERS_2:def 9;
hence ( [a,b] in FinOrd R or [b,a] in FinOrd R ) by A1, A6, A7, A8, Th40; :: thesis: verum

end;

end;

end;

hence ( [a,b] in FinOrd R or [b,a] in FinOrd R ) ; :: thesis: verum

end;

suppose A9: PosetMax a = PosetMax b ; :: thesis: ( [a,b] in FinOrd R or [b,a] in FinOrd R )

set ax = a \ {(PosetMax a)};
set bx = b \ {(PosetMax b)};
A10: card (a \ {(PosetMax a)}) = n by A5, Lm1;
reconsider ax = a \ {(PosetMax a)}, bx = b \ {(PosetMax b)} as Element of Fin the carrier of R by Th38;

now

per cases ( [ax,bx] in FinOrd R or [bx,ax] in FinOrd R ) by A4, A10;

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, A6, A7, A9, Th40; :: 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, A6, A7, A9, Th40; :: 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 A11: for n being Element of NAT st S₁[n] holds
S₁[n + 1] ;
A12: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A3, A11);
consider n being Nat such that
A13: x,n are_equipotent by CARD_1:74;
card x' = n by A13, CARD_1:def 5;
then ( [x',y'] in FinOrd R or [y',x'] in FinOrd R ) by A12;
hence ( x <= y or y <= x ) by ORDERS_2:def 9; :: thesis: verum

end;

hence FinPoset R is connected by WAYBEL_0:def 29; :: thesis: verum