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 :: thesis: for x, y being Element of (FinPoset R) holds
( x <= y or y <= x )

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

end;

then A2: S₁[ 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 [b₄,b₅] in FinOrd R or [b₅,b₄] 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 [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 A4: 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, Th36; :: thesis: verum

end;

suppose A5: a <> {} ; :: thesis: ( [b₂,b₃] in FinOrd R or [b₃,b₂] 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 A1, Th36; :: 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 ( PosetMax a <> PosetMax b or PosetMax a = PosetMax b ) ;

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 ( 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 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 [(PosetMax b),(PosetMax a)] 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 \ {(PosetMax a)};
set bx = b \ {(PosetMax b)};
A9: card (a \ {(PosetMax a)}) = n by A4, Lm1;
reconsider ax = a \ {(PosetMax a)}, bx = b \ {(PosetMax 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 S₁[n] holds
S₁[n + 1] ;
A11: for n being Nat holds S₁[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