defpred S_{1}[ Nat] means for A being finite Chain st card the carrier of A = $1 holds

A, InclPoset $1 are_isomorphic ;

A1: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A36, A1);

hence for A being finite Chain

for n being Nat st card the carrier of A = n holds

A, InclPoset n are_isomorphic ; :: thesis: verum

A, InclPoset $1 are_isomorphic ;

A1: for n being Nat st S

S

proof

A36:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A2: for A being finite Chain st card the carrier of A = n holds

A, InclPoset n are_isomorphic ; :: thesis: S_{1}[n + 1]

n >= 0 by NAT_1:2;

then n + 1 >= 0 + 1 by XREAL_1:6;

then A3: ( n >= 1 or n + 1 = 1 ) by NAT_1:8;

let A be finite Chain ; :: thesis: ( card the carrier of A = n + 1 implies A, InclPoset (n + 1) are_isomorphic )

assume A4: card the carrier of A = n + 1 ; :: thesis: A, InclPoset (n + 1) are_isomorphic

then reconsider A = A as non empty finite Chain ;

set b = Top A;

end;assume A2: for A being finite Chain st card the carrier of A = n holds

A, InclPoset n are_isomorphic ; :: thesis: S

n >= 0 by NAT_1:2;

then n + 1 >= 0 + 1 by XREAL_1:6;

then A3: ( n >= 1 or n + 1 = 1 ) by NAT_1:8;

let A be finite Chain ; :: thesis: ( card the carrier of A = n + 1 implies A, InclPoset (n + 1) are_isomorphic )

assume A4: card the carrier of A = n + 1 ; :: thesis: A, InclPoset (n + 1) are_isomorphic

then reconsider A = A as non empty finite Chain ;

set b = Top A;

per cases
( n + 1 = 1 or n + 1 > 1 )
by A3, NAT_1:13;

end;

suppose A5:
n + 1 = 1
; :: thesis: A, InclPoset (n + 1) are_isomorphic

then consider x being object such that

A6: the carrier of A = {x} by A4, CARD_2:42;

A, InclPoset 1 are_isomorphic

end;A6: the carrier of A = {x} by A4, CARD_2:42;

A, InclPoset 1 are_isomorphic

proof

hence
A, InclPoset (n + 1) are_isomorphic
by A5; :: thesis: verum
set g = the carrier of A --> 0;

A7: rng ( the carrier of A --> 0) = {0} by FUNCOP_1:8;

A8: {0} = the carrier of (InclPoset 1) by CARD_1:49, YELLOW_1:1;

then reconsider g = the carrier of A --> 0 as Function of A,(InclPoset 1) ;

A9: for e, f being Element of A holds

( e <= f iff g . e <= g . f )

hence A, InclPoset 1 are_isomorphic ; :: thesis: verum

end;A7: rng ( the carrier of A --> 0) = {0} by FUNCOP_1:8;

A8: {0} = the carrier of (InclPoset 1) by CARD_1:49, YELLOW_1:1;

then reconsider g = the carrier of A --> 0 as Function of A,(InclPoset 1) ;

A9: for e, f being Element of A holds

( e <= f iff g . e <= g . f )

proof

g is V13()
let e, f be Element of A; :: thesis: ( e <= f iff g . e <= g . f )

e = x by A6, TARSKI:def 1;

hence e <= f by A6, TARSKI:def 1; :: thesis: verum

end;hereby :: thesis: ( g . e <= g . f implies e <= f )

assume
g . e <= g . f
; :: thesis: e <= fassume
e <= f
; :: thesis: g . e <= g . f

g . e = 0 by FUNCOP_1:7;

hence g . e <= g . f by FUNCOP_1:7; :: thesis: verum

end;g . e = 0 by FUNCOP_1:7;

hence g . e <= g . f by FUNCOP_1:7; :: thesis: verum

e = x by A6, TARSKI:def 1;

hence e <= f by A6, TARSKI:def 1; :: thesis: verum

proof

then
g is isomorphic
by A7, A8, A9, WAYBEL_0:66;
let x1, x2 be Element of A; :: according to WAYBEL_1:def 1 :: thesis: ( not g . x1 = g . x2 or x1 = x2 )

assume g . x1 = g . x2 ; :: thesis: x1 = x2

x1 = x by A6, TARSKI:def 1;

hence x1 = x2 by A6, TARSKI:def 1; :: thesis: verum

end;assume g . x1 = g . x2 ; :: thesis: x1 = x2

x1 = x by A6, TARSKI:def 1;

hence x1 = x2 by A6, TARSKI:def 1; :: thesis: verum

hence A, InclPoset 1 are_isomorphic ; :: thesis: verum

suppose A10:
n + 1 > 1
; :: thesis: A, InclPoset (n + 1) are_isomorphic

A11: card ( the carrier of A \ {(Top A)}) =
(card the carrier of A) - (card {(Top A)})
by CARD_2:44

.= (n + 1) - 1 by A4, CARD_1:30

.= n ;

(n + 1) - 1 > 1 - 1 by A10, XREAL_1:9;

then reconsider Ab = the carrier of A \ {(Top A)} as non empty Subset of A by A11;

reconsider B = subrelstr Ab as finite Chain by Def1;

card the carrier of B = n by A11, YELLOW_0:def 15;

then B, InclPoset n are_isomorphic by A2;

then consider f being Function of B,(InclPoset n) such that

A12: f is isomorphic ;

the carrier of B = the carrier of A \ {(Top A)} by YELLOW_0:def 15;

then A13: the carrier of B,{(Top A)} form_upper_lower_partition_of A by Th3;

A14: Segm (n + 1) = (Segm n) \/ {n} by AFINSQ_1:2;

then {n} c= Segm (n + 1) by XBOOLE_1:7;

then reconsider n9 = {n} as non empty Subset of (InclPoset (n + 1)) by YELLOW_1:1;

set X = InclPoset {(Top A)};

A15: the carrier of (subrelstr n9) = n9 by YELLOW_0:def 15;

{(Top A)} c= {(Top A)} ;

then reconsider b9 = {(Top A)} as non empty Subset of (InclPoset {(Top A)}) by YELLOW_1:1;

set X9 = subrelstr b9;

set g = the carrier of (subrelstr b9) --> n;

dom ( the carrier of (subrelstr b9) --> n) = the carrier of (subrelstr b9) by FUNCOP_1:13;

then reconsider g = the carrier of (subrelstr b9) --> n as ManySortedSet of the carrier of (subrelstr b9) by PARTFUN1:def 2;

A16: for a, b being Element of (InclPoset (n + 1)) st a in the carrier of (InclPoset n) & b in {n} holds

a < b

then the carrier of (InclPoset n) \/ {n} = the carrier of (InclPoset (n + 1)) by A14, YELLOW_1:1;

then A28: the carrier of (InclPoset n),{n} form_upper_lower_partition_of InclPoset (n + 1) by A16;

n <= n + 1 by NAT_1:11;

then Segm n c= Segm (n + 1) by NAT_1:39;

then n c= the carrier of (InclPoset (n + 1)) by YELLOW_1:1;

then reconsider A2 = the carrier of (InclPoset n) as Subset of (InclPoset (n + 1)) by YELLOW_1:1;

A29: the carrier of (subrelstr {(Top A)}) = {(Top A)} by YELLOW_0:def 15;

A30: the carrier of (subrelstr b9) = {(Top A)} by YELLOW_0:def 15;

then reconsider g = g as Function of (subrelstr {(Top A)}),(subrelstr n9) by A15, A29;

g . (Top A) in n9 by A15, A29, FUNCT_2:47;

then g . (Top A) = n by TARSKI:def 1;

then A31: rng g = the carrier of (subrelstr n9) by A15, A29, FUNCT_2:48;

A32: for e, f being Element of (subrelstr {(Top A)}) holds

( e <= f iff g . e <= g . f )

then A34: g is isomorphic by A31, A32, WAYBEL_0:66;

InclPoset n is full SubRelStr of InclPoset (n + 1) by Th1, NAT_1:11;

then A35: InclPoset n = subrelstr A2 by YELLOW_0:def 15;

the carrier of B = Ab by YELLOW_0:def 15;

then ex h being Function of A,(InclPoset (n + 1)) st

( h = f +* g & h is isomorphic ) by A12, A13, A28, A34, A35, Th5;

hence A, InclPoset (n + 1) are_isomorphic ; :: thesis: verum

end;.= (n + 1) - 1 by A4, CARD_1:30

.= n ;

(n + 1) - 1 > 1 - 1 by A10, XREAL_1:9;

then reconsider Ab = the carrier of A \ {(Top A)} as non empty Subset of A by A11;

reconsider B = subrelstr Ab as finite Chain by Def1;

card the carrier of B = n by A11, YELLOW_0:def 15;

then B, InclPoset n are_isomorphic by A2;

then consider f being Function of B,(InclPoset n) such that

A12: f is isomorphic ;

the carrier of B = the carrier of A \ {(Top A)} by YELLOW_0:def 15;

then A13: the carrier of B,{(Top A)} form_upper_lower_partition_of A by Th3;

A14: Segm (n + 1) = (Segm n) \/ {n} by AFINSQ_1:2;

then {n} c= Segm (n + 1) by XBOOLE_1:7;

then reconsider n9 = {n} as non empty Subset of (InclPoset (n + 1)) by YELLOW_1:1;

set X = InclPoset {(Top A)};

A15: the carrier of (subrelstr n9) = n9 by YELLOW_0:def 15;

{(Top A)} c= {(Top A)} ;

then reconsider b9 = {(Top A)} as non empty Subset of (InclPoset {(Top A)}) by YELLOW_1:1;

set X9 = subrelstr b9;

set g = the carrier of (subrelstr b9) --> n;

dom ( the carrier of (subrelstr b9) --> n) = the carrier of (subrelstr b9) by FUNCOP_1:13;

then reconsider g = the carrier of (subrelstr b9) --> n as ManySortedSet of the carrier of (subrelstr b9) by PARTFUN1:def 2;

A16: for a, b being Element of (InclPoset (n + 1)) st a in the carrier of (InclPoset n) & b in {n} holds

a < b

proof

the carrier of (InclPoset n) = n
by YELLOW_1:1;
let a, b be Element of (InclPoset (n + 1)); :: thesis: ( a in the carrier of (InclPoset n) & b in {n} implies a < b )

assume that

A17: a in the carrier of (InclPoset n) and

A18: b in {n} ; :: thesis: a < b

A19: a in n by A17, YELLOW_1:1;

then a in { i where i is Nat : i < n } by AXIOMS:4;

then consider h being Nat such that

A20: h = a and

A21: h < n ;

A22: b = n by A18, TARSKI:def 1;

a c= b

a <> b by A19, A22;

hence a < b by A27, ORDERS_2:def 6; :: thesis: verum

end;assume that

A17: a in the carrier of (InclPoset n) and

A18: b in {n} ; :: thesis: a < b

A19: a in n by A17, YELLOW_1:1;

then a in { i where i is Nat : i < n } by AXIOMS:4;

then consider h being Nat such that

A20: h = a and

A21: h < n ;

A22: b = n by A18, TARSKI:def 1;

a c= b

proof

then A27:
a <= b
by YELLOW_1:3;
assume
not a c= b
; :: thesis: contradiction

then consider x being object such that

A23: x in a and

A24: not x in b ;

x in { w where w is Nat : w < h } by A20, A23, AXIOMS:4;

then consider w9 being Nat such that

A25: w9 = x and

A26: w9 < h ;

w9 < n by A21, A26, XXREAL_0:2;

then w9 in { t where t is Nat : t < n } ;

hence contradiction by A22, A24, A25, AXIOMS:4; :: thesis: verum

end;then consider x being object such that

A23: x in a and

A24: not x in b ;

x in { w where w is Nat : w < h } by A20, A23, AXIOMS:4;

then consider w9 being Nat such that

A25: w9 = x and

A26: w9 < h ;

w9 < n by A21, A26, XXREAL_0:2;

then w9 in { t where t is Nat : t < n } ;

hence contradiction by A22, A24, A25, AXIOMS:4; :: thesis: verum

a <> b by A19, A22;

hence a < b by A27, ORDERS_2:def 6; :: thesis: verum

then the carrier of (InclPoset n) \/ {n} = the carrier of (InclPoset (n + 1)) by A14, YELLOW_1:1;

then A28: the carrier of (InclPoset n),{n} form_upper_lower_partition_of InclPoset (n + 1) by A16;

n <= n + 1 by NAT_1:11;

then Segm n c= Segm (n + 1) by NAT_1:39;

then n c= the carrier of (InclPoset (n + 1)) by YELLOW_1:1;

then reconsider A2 = the carrier of (InclPoset n) as Subset of (InclPoset (n + 1)) by YELLOW_1:1;

A29: the carrier of (subrelstr {(Top A)}) = {(Top A)} by YELLOW_0:def 15;

A30: the carrier of (subrelstr b9) = {(Top A)} by YELLOW_0:def 15;

then reconsider g = g as Function of (subrelstr {(Top A)}),(subrelstr n9) by A15, A29;

g . (Top A) in n9 by A15, A29, FUNCT_2:47;

then g . (Top A) = n by TARSKI:def 1;

then A31: rng g = the carrier of (subrelstr n9) by A15, A29, FUNCT_2:48;

A32: for e, f being Element of (subrelstr {(Top A)}) holds

( e <= f iff g . e <= g . f )

proof

g is V13()
by A29, PARTFUN1:17;
let e, f be Element of (subrelstr {(Top A)}); :: thesis: ( e <= f iff g . e <= g . f )

reconsider f1 = f as Element of (subrelstr b9) by A30, YELLOW_0:def 15;

reconsider e1 = e as Element of (subrelstr b9) by A30, YELLOW_0:def 15;

e in the carrier of (subrelstr {(Top A)}) ;

then e in {(Top A)} by YELLOW_0:def 15;

then A33: e = Top A by TARSKI:def 1;

f in the carrier of (subrelstr {(Top A)}) ;

then f in {(Top A)} by YELLOW_0:def 15;

hence e <= f by A33, TARSKI:def 1; :: thesis: verum

end;reconsider f1 = f as Element of (subrelstr b9) by A30, YELLOW_0:def 15;

reconsider e1 = e as Element of (subrelstr b9) by A30, YELLOW_0:def 15;

hereby :: thesis: ( g . e <= g . f implies e <= f )

assume
g . e <= g . f
; :: thesis: e <= fassume
e <= f
; :: thesis: g . e <= g . f

( g . e1 = n & g . f1 = n ) by FUNCOP_1:7;

hence g . e <= g . f ; :: thesis: verum

end;( g . e1 = n & g . f1 = n ) by FUNCOP_1:7;

hence g . e <= g . f ; :: thesis: verum

e in the carrier of (subrelstr {(Top A)}) ;

then e in {(Top A)} by YELLOW_0:def 15;

then A33: e = Top A by TARSKI:def 1;

f in the carrier of (subrelstr {(Top A)}) ;

then f in {(Top A)} by YELLOW_0:def 15;

hence e <= f by A33, TARSKI:def 1; :: thesis: verum

then A34: g is isomorphic by A31, A32, WAYBEL_0:66;

InclPoset n is full SubRelStr of InclPoset (n + 1) by Th1, NAT_1:11;

then A35: InclPoset n = subrelstr A2 by YELLOW_0:def 15;

the carrier of B = Ab by YELLOW_0:def 15;

then ex h being Function of A,(InclPoset (n + 1)) st

( h = f +* g & h is isomorphic ) by A12, A13, A28, A34, A35, Th5;

hence A, InclPoset (n + 1) are_isomorphic ; :: thesis: verum

proof

for n being Nat holds S
let A be finite Chain ; :: thesis: ( card the carrier of A = 0 implies A, InclPoset 0 are_isomorphic )

set f = the Function of A,(InclPoset 0);

assume card the carrier of A = 0 ; :: thesis: A, InclPoset 0 are_isomorphic

then A37: A is empty ;

take the Function of A,(InclPoset 0) ; :: according to WAYBEL_1:def 8 :: thesis: the Function of A,(InclPoset 0) is isomorphic

InclPoset 0 is empty by YELLOW_1:1;

hence the Function of A,(InclPoset 0) is isomorphic by A37, WAYBEL_0:def 38; :: thesis: verum

end;set f = the Function of A,(InclPoset 0);

assume card the carrier of A = 0 ; :: thesis: A, InclPoset 0 are_isomorphic

then A37: A is empty ;

take the Function of A,(InclPoset 0) ; :: according to WAYBEL_1:def 8 :: thesis: the Function of A,(InclPoset 0) is isomorphic

InclPoset 0 is empty by YELLOW_1:1;

hence the Function of A,(InclPoset 0) is isomorphic by A37, WAYBEL_0:def 38; :: thesis: verum

hence for A being finite Chain

for n being Nat st card the carrier of A = n holds

A, InclPoset n are_isomorphic ; :: thesis: verum