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) #) ;

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 )

hence
FinPoset R is connected
by WAYBEL_0:def 29; :: thesis: verum( 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_{1}[ 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 );

_{1}[ 0 ]
;

_{1}[n] holds

S_{1}[n + 1]
;

A11: for n being Nat holds S_{1}[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;reconsider x9 = x, y9 = y as Element of Fin the carrier of R ;

defpred S

( 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 )

then A2:
S( 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;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

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 )

then A10:
for n being Nat st S( 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_{4},b_{5}] in FinOrd R or [b_{5},b_{4}] 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_{4},b_{5}] in FinOrd R or [b_{5},b_{4}] in FinOrd R )

let a, b be Element of Fin the carrier of R; :: thesis: ( not card a = n + 1 or [b_{2},b_{3}] in FinOrd R or [b_{3},b_{2}] in FinOrd R )

assume A4: card a = n + 1 ; :: thesis: ( [b_{2},b_{3}] in FinOrd R or [b_{3},b_{2}] in FinOrd R )

end;( 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

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

let a, b be Element of Fin the carrier of R; :: thesis: ( not card a = n + 1 or [b

assume A4: card a = n + 1 ; :: thesis: ( [b

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

end;

suppose A5:
a <> {}
; :: thesis: ( [b_{2},b_{3}] in FinOrd R or [b_{3},b_{2}] in FinOrd R )

end;

now :: thesis: ( [a,b] in FinOrd R or [b,a] in FinOrd R )end;

hence
( [a,b] in FinOrd R or [b,a] in FinOrd R )
; :: thesis: verumper cases
( b = {} or b <> {} )
;

end;

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

end;

now :: thesis: ( [a,b] in FinOrd R or [b,a] in FinOrd R )end;

hence
( [a,b] in FinOrd R or [b,a] in FinOrd R )
; :: thesis: verumper cases
( PosetMax a <> PosetMax b or PosetMax a = PosetMax b )
;

end;

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

end;

now :: thesis: ( [a,b] in FinOrd R or [b,a] in FinOrd R )end;

hence
( [a,b] in FinOrd R or [b,a] in FinOrd R )
; :: thesis: verumper cases
( PosetMax a <= PosetMax b or PosetMax b <= PosetMax a )
by WAYBEL_0:def 29;

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;

end;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 )

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

S

A11: for n being Nat holds S

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