:: ORDERS_4 semantic presentation

begin

definition
mode Chain  ->  RelStr  means :Def1: :: ORDERS_4:def 1
( it is non empty connected Poset or it is empty );
existence
 ex b1 being RelStr st
( b1 is non empty connected Poset or b1 is empty )
proof
set R = the empty RelStr ;
take  the empty RelStr ; ::_thesis: ( the empty RelStr is non empty connected Poset or the empty RelStr is empty )
thus  ( the empty RelStr is non empty connected Poset or the empty RelStr is empty ) ; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines Chain ORDERS_4:def_1_:_
 for b1 being RelStr holds
( b1 is Chain iff ( b1 is non empty connected Poset or b1 is empty ) );

registration
cluster empty  ->  reflexive transitive antisymmetric for RelStr ;
coherence
 for b1 being RelStr st b1 is empty holds
( b1 is reflexive & b1 is transitive & b1 is antisymmetric )
proof
let A be RelStr ; ::_thesis: ( A is empty implies ( A is reflexive & A is transitive & A is antisymmetric ) )
assume A1: A is empty ; ::_thesis: ( A is reflexive & A is transitive & A is antisymmetric )
then  for x, y, z being set st x in the carrier of A & y in the carrier of A & z in the carrier of A & [x,y] in the InternalRel of A & [y,z] in the InternalRel of A holds
[x,z] in the InternalRel of A ;
then A2: the InternalRel of A is_transitive_in the carrier of A by RELAT_2:def_8;
 for x, y being set st x in the carrier of A & y in the carrier of A & [x,y] in the InternalRel of A & [y,x] in the InternalRel of A holds
x = y by A1;
then A3: the InternalRel of A is_antisymmetric_in the carrier of A by RELAT_2:def_4;
 for x being set st x in the carrier of A holds
[x,x] in the InternalRel of A by A1;
then  the InternalRel of A is_reflexive_in the carrier of A by RELAT_2:def_1;
hence  ( A is reflexive & A is transitive & A is antisymmetric ) by A2, A3, ORDERS_2:def_2, ORDERS_2:def_3, ORDERS_2:def_4; ::_thesis: verum
end;
end;

registration
cluster  ->  reflexive transitive antisymmetric for Chain ;
coherence
 for b1 being Chain holds
( b1 is reflexive & b1 is transitive & b1 is antisymmetric )
proof
let A be Chain ; ::_thesis: ( A is reflexive & A is transitive & A is antisymmetric )
 ( A is non empty connected Poset or A is empty RelStr ) by Def1;
hence  ( A is reflexive & A is transitive & A is antisymmetric ) ; ::_thesis: verum
end;
end;

registration
cluster non empty V80() reflexive transitive antisymmetric for Chain ;
existence
 not for b1 being Chain holds b1 is empty
proof
set A = the non empty trivial reflexive transitive antisymmetric RelStr ;
 the non empty trivial reflexive transitive antisymmetric RelStr is Chain by Def1;
hence  not for b1 being Chain holds b1 is empty ; ::_thesis: verum
end;
end;

registration
cluster non empty  ->  non empty connected for Chain ;
coherence
 for b1 being non empty Chain holds b1 is connected by Def1;
end;

definition
let L be 1-sorted ;
attrL is countable  means :Def2: :: ORDERS_4:def 2
 the carrier of L is countable ;
end;

:: deftheorem Def2 defines countable ORDERS_4:def_2_:_
 for L being 1-sorted holds
( L is countable iff the carrier of L is countable );

registration
cluster non empty finite V80() reflexive transitive antisymmetric for Chain ;
existence
 ex b1 being Chain st
( b1 is finite & not b1 is empty )
proof
set A = the non empty trivial finite reflexive transitive antisymmetric RelStr ;
 the non empty trivial finite reflexive transitive antisymmetric RelStr is Chain by Def1;
hence  ex b1 being Chain st
( b1 is finite & not b1 is empty ) ; ::_thesis: verum
end;
end;

registration
clusterV80() reflexive transitive antisymmetric countable for Chain ;
existence
 ex b1 being Chain st b1 is countable
proof
set L = the finite Chain ;
take  the finite Chain ; ::_thesis: the finite Chain is countable
 the carrier of the finite Chain is countable by CARD_4:1;
hence  the finite Chain is countable by Def2; ::_thesis: verum
end;
end;

registration
let A be non empty connected RelStr ;
cluster non empty full  ->  non empty connected for SubRelStr of A;
correctness
coherence
for b1 being non empty SubRelStr of A st b1 is full holds
b1 is connected ;
proof
let S be non empty SubRelStr of A; ::_thesis: ( S is full implies S is connected )
assume A1: S is full ; ::_thesis: S is connected
 for x, y being Element of S holds
( x <= y or y <= x )
proof
let x, y be Element of S; ::_thesis: ( x <= y or y <= x )
A2: the carrier of S c= the carrier of A by YELLOW_0:def_13;
 y in the carrier of S ;
then reconsider b = y as Element of A by A2;
 x in the carrier of S ;
then reconsider a = x as Element of A by A2;
 ( a <= b or b <= a ) by WAYBEL_0:def_29;
hence  ( x <= y or y <= x ) by A1, YELLOW_0:60; ::_thesis: verum
end;
hence  S is connected by WAYBEL_0:def_29; ::_thesis: verum
end;
end;

registration
let A be finite RelStr ;
cluster  ->  finite for SubRelStr of A;
correctness
coherence
for b1 being SubRelStr of A holds b1 is finite ;
proof
let S be SubRelStr of A; ::_thesis: S is finite
 the carrier of S c= the carrier of A by YELLOW_0:def_13;
hence  S is finite ; ::_thesis: verum
end;
end;

theorem Th1: :: ORDERS_4:1
for n, m being Nat st n <= m holds
InclPoset n is full SubRelStr of InclPoset m
proof
let n, m be Nat; ::_thesis: ( n <= m implies InclPoset n is full SubRelStr of InclPoset m )
A1: the InternalRel of (InclPoset m) = RelIncl m by YELLOW_1:1;
assume  n <= m ; ::_thesis: InclPoset n is full SubRelStr of InclPoset m
then A2: n c= m by NAT_1:39;
A3: RelIncl n c= RelIncl m
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in RelIncl n or x in RelIncl m )
assume  x in RelIncl n ; ::_thesis: x in RelIncl m
then  x in (RelIncl m) |_2 n by A2, WELLORD2:7;
hence  x in RelIncl m by XBOOLE_0:def_4; ::_thesis: verum
end;
 the carrier of (InclPoset m) = m by YELLOW_1:1;
then A4: the carrier of (InclPoset n) c= the carrier of (InclPoset m) by A2, YELLOW_1:1;
A5: the InternalRel of (InclPoset n) = RelIncl n by YELLOW_1:1;
then  (RelIncl m) |_2 n = the InternalRel of (InclPoset n) by A2, WELLORD2:7;
then  the InternalRel of (InclPoset n) = the InternalRel of (InclPoset m) |_2 the carrier of (InclPoset n) by A1, YELLOW_1:1;
hence  InclPoset n is full SubRelStr of InclPoset m by A4, A5, A1, A3, YELLOW_0:def_13, YELLOW_0:def_14; ::_thesis: verum
end;

definition
let L be RelStr ;
let A, B be set ;
predA,B form_upper_lower_partition_of L means :Def3: :: ORDERS_4:def 3
( A \/ B = the carrier of L & ( for a, b being Element of L st a in A & b in B holds
a < b ) );
end;

:: deftheorem Def3 defines form_upper_lower_partition_of ORDERS_4:def_3_:_
 for L being RelStr
for A, B being set holds
( A,B form_upper_lower_partition_of L iff ( A \/ B = the carrier of L & ( for a, b being Element of L st a in A & b in B holds
a < b ) ) );

theorem Th2: :: ORDERS_4:2
for L being RelStr
for A, B being set st A,B form_upper_lower_partition_of L holds
A misses B
proof
let L be RelStr ; ::_thesis: for A, B being set st A,B form_upper_lower_partition_of L holds
A misses B
let A, B be set ; ::_thesis: ( A,B form_upper_lower_partition_of L implies A misses B )
assume that
A1: A,B form_upper_lower_partition_of L and
A2: A meets B ; ::_thesis: contradiction
consider x being set  such that
A3: x in A /\ B by A2, XBOOLE_0:4;
A4: x in B by A3, XBOOLE_0:def_4;
A5: x in A by A3, XBOOLE_0:def_4;
 A \/ B = the carrier of L by A1, Def3;
then reconsider x = x as Element of L by A5, XBOOLE_0:def_3;
 x < x by A1, A5, A4, Def3;
hence  contradiction ; ::_thesis: verum
end;

theorem Th3: :: ORDERS_4:3
for L being non empty antisymmetric upper-bounded RelStr holds the carrier of L \ {(Top L)},{(Top L)} form_upper_lower_partition_of L
proof
let L be non empty antisymmetric upper-bounded RelStr ; ::_thesis: the carrier of L \ {(Top L)},{(Top L)} form_upper_lower_partition_of L
A1: for a, b being Element of L st a in the carrier of L \ {(Top L)} & b in {(Top L)} holds
a < b
proof
let a, b be Element of L; ::_thesis: ( a in the carrier of L \ {(Top L)} & b in {(Top L)} implies a < b )
assume that
A2: a in the carrier of L \ {(Top L)} and
A3: b in {(Top L)} ; ::_thesis: a < b
 not a in {(Top L)} by A2, XBOOLE_0:def_5;
then A4: a <> Top L by TARSKI:def_1;
A5: a <= Top L by YELLOW_0:45;
 b = Top L by A3, TARSKI:def_1;
hence  a < b by A4, A5, ORDERS_2:def_6; ::_thesis: verum
end;
 ( the carrier of L \ {(Top L)}) \/ {(Top L)} = the carrier of L by XBOOLE_1:45;
hence  the carrier of L \ {(Top L)},{(Top L)} form_upper_lower_partition_of L by A1, Def3; ::_thesis: verum
end;

theorem Th4: :: ORDERS_4:4
for L1, L2 being RelStr
for f being Function of L1,L2 st f is isomorphic holds
( ( the carrier of L1 <> {} implies the carrier of L2 <> {} ) & ( the carrier of L2 <> {} implies the carrier of L1 <> {} ) & ( the carrier of L2 <> {} or the carrier of L1 = {} ) & ( the carrier of L1 = {} implies the carrier of L2 = {} ) & ( the carrier of L2 = {} implies the carrier of L1 = {} ) )
proof
let L1, L2 be RelStr ; ::_thesis: for f being Function of L1,L2 st f is isomorphic holds
( ( the carrier of L1 <> {} implies the carrier of L2 <> {} ) & ( the carrier of L2 <> {} implies the carrier of L1 <> {} ) & ( the carrier of L2 <> {} or the carrier of L1 = {} ) & ( the carrier of L1 = {} implies the carrier of L2 = {} ) & ( the carrier of L2 = {} implies the carrier of L1 = {} ) )
let f be Function of L1,L2; ::_thesis: ( f is isomorphic implies ( ( the carrier of L1 <> {} implies the carrier of L2 <> {} ) & ( the carrier of L2 <> {} implies the carrier of L1 <> {} ) & ( the carrier of L2 <> {} or the carrier of L1 = {} ) & ( the carrier of L1 = {} implies the carrier of L2 = {} ) & ( the carrier of L2 = {} implies the carrier of L1 = {} ) ) )
assume A1: f is isomorphic ; ::_thesis: ( ( the carrier of L1 <> {} implies the carrier of L2 <> {} ) & ( the carrier of L2 <> {} implies the carrier of L1 <> {} ) & ( the carrier of L2 <> {} or the carrier of L1 = {} ) & ( the carrier of L1 = {} implies the carrier of L2 = {} ) & ( the carrier of L2 = {} implies the carrier of L1 = {} ) )
 ( the carrier of L1 = {} iff the carrier of L2 = {} )
proof
hereby  ::_thesis: ( the carrier of L2 = {} implies the carrier of L1 = {} )
assume  the carrier of L1 = {} ; ::_thesis: the carrier of L2 = {}
then  L1 is empty ;
then  L2 is empty by A1, WAYBEL_0:def_38;
hence  the carrier of L2 = {} ; ::_thesis: verum
end;
assume  the carrier of L2 = {} ; ::_thesis: the carrier of L1 = {}
then  L2 is empty ;
then  L1 is empty by A1, WAYBEL_0:def_38;
hence  the carrier of L1 = {} ; ::_thesis: verum
end;
hence  ( ( the carrier of L1 <> {} implies the carrier of L2 <> {} ) & ( the carrier of L2 <> {} implies the carrier of L1 <> {} ) & ( the carrier of L2 <> {} or the carrier of L1 = {} ) & ( the carrier of L1 = {} implies the carrier of L2 = {} ) & ( the carrier of L2 = {} implies the carrier of L1 = {} ) ) ; ::_thesis: verum
end;

theorem Th5: :: ORDERS_4:5
for L1, L2 being antisymmetric RelStr
for A1, B1 being Subset of L1 st A1,B1 form_upper_lower_partition_of L1 holds
for A2, B2 being Subset of L2 st A2,B2 form_upper_lower_partition_of L2 holds
for f being Function of (subrelstr A1),(subrelstr A2) st f is isomorphic holds
for g being Function of (subrelstr B1),(subrelstr B2) st g is isomorphic holds
ex h being Function of L1,L2 st
( h = f +* g & h is isomorphic )
proof
let L1, L2 be antisymmetric RelStr ; ::_thesis: for A1, B1 being Subset of L1 st A1,B1 form_upper_lower_partition_of L1 holds
for A2, B2 being Subset of L2 st A2,B2 form_upper_lower_partition_of L2 holds
for f being Function of (subrelstr A1),(subrelstr A2) st f is isomorphic holds
for g being Function of (subrelstr B1),(subrelstr B2) st g is isomorphic holds
ex h being Function of L1,L2 st
( h = f +* g & h is isomorphic )
let A1, B1 be Subset of L1; ::_thesis: ( A1,B1 form_upper_lower_partition_of L1 implies for A2, B2 being Subset of L2 st A2,B2 form_upper_lower_partition_of L2 holds
for f being Function of (subrelstr A1),(subrelstr A2) st f is isomorphic holds
for g being Function of (subrelstr B1),(subrelstr B2) st g is isomorphic holds
ex h being Function of L1,L2 st
( h = f +* g & h is isomorphic ) )
assume A1: A1,B1 form_upper_lower_partition_of L1 ; ::_thesis: for A2, B2 being Subset of L2 st A2,B2 form_upper_lower_partition_of L2 holds
for f being Function of (subrelstr A1),(subrelstr A2) st f is isomorphic holds
for g being Function of (subrelstr B1),(subrelstr B2) st g is isomorphic holds
ex h being Function of L1,L2 st
( h = f +* g & h is isomorphic )
A2: A1 \/ B1 = the carrier of L1 by A1, Def3;
let A2, B2 be Subset of L2; ::_thesis: ( A2,B2 form_upper_lower_partition_of L2 implies for f being Function of (subrelstr A1),(subrelstr A2) st f is isomorphic holds
for g being Function of (subrelstr B1),(subrelstr B2) st g is isomorphic holds
ex h being Function of L1,L2 st
( h = f +* g & h is isomorphic ) )
assume A3: A2,B2 form_upper_lower_partition_of L2 ; ::_thesis: for f being Function of (subrelstr A1),(subrelstr A2) st f is isomorphic holds
for g being Function of (subrelstr B1),(subrelstr B2) st g is isomorphic holds
ex h being Function of L1,L2 st
( h = f +* g & h is isomorphic )
A4: A2 misses B2 by A3, Th2;
A5: A2 \/ B2 = the carrier of L2 by A3, Def3;
A6: A1 misses B1 by A1, Th2;
let f be Function of (subrelstr A1),(subrelstr A2); ::_thesis: ( f is isomorphic implies for g being Function of (subrelstr B1),(subrelstr B2) st g is isomorphic holds
ex h being Function of L1,L2 st
( h = f +* g & h is isomorphic ) )
assume A7: f is isomorphic ; ::_thesis: for g being Function of (subrelstr B1),(subrelstr B2) st g is isomorphic holds
ex h being Function of L1,L2 st
( h = f +* g & h is isomorphic )
let g be Function of (subrelstr B1),(subrelstr B2); ::_thesis: ( g is isomorphic implies ex h being Function of L1,L2 st
( h = f +* g & h is isomorphic ) )
assume A8: g is isomorphic ; ::_thesis: ex h being Function of L1,L2 st
( h = f +* g & h is isomorphic )
set h = f +* g;
percases ( the carrier of L1 = {} or the carrier of L1 <> {} ) ;
supposeA9: the carrier of L1 = {} ; ::_thesis: ex h being Function of L1,L2 st
( h = f +* g & h is isomorphic )
then A10: A1 = {} by A2;
then  the carrier of (subrelstr A1) = {} by YELLOW_0:def_15;
then  dom f = the carrier of (subrelstr A1) ;
then A11: dom f = A1 by YELLOW_0:def_15;
 subrelstr A1 is empty by A10, YELLOW_0:def_15;
then  subrelstr A2 is empty by A7, WAYBEL_0:def_38;
then A12: A2 = {} by YELLOW_0:def_15;
A13: for x being set st x in the carrier of L1 holds
(f +* g) . x in the carrier of L2 by A9;
A14: B1 = {} by A2, A9;
then  ( the carrier of (subrelstr B2) <> {} or the carrier of (subrelstr B1) = {} ) by YELLOW_0:def_15;
then  dom g = the carrier of (subrelstr B1) by FUNCT_2:def_1;
then  dom g = B1 by YELLOW_0:def_15;
then  dom (f +* g) = the carrier of L1 by A2, A11, FUNCT_4:def_1;
then reconsider h = f +* g as Function of L1,L2 by A13, FUNCT_2:3;
A15: L1 is empty by A9;
 subrelstr B1 is empty by A14, YELLOW_0:def_15;
then  L2 is empty by A8, A5, A12, WAYBEL_0:def_38;
then  h is isomorphic by A15, WAYBEL_0:def_38;
hence  ex h being Function of L1,L2 st
( h = f +* g & h is isomorphic ) ; ::_thesis: verum
end;
supposeA16: the carrier of L1 <> {} ; ::_thesis: ex h being Function of L1,L2 st
( h = f +* g & h is isomorphic )
then  ( A1 <> {} or B1 <> {} ) by A2;
then  ( not subrelstr A1 is empty or not subrelstr B1 is empty ) by YELLOW_0:def_15;
then A17: ( not subrelstr A2 is empty or not subrelstr B2 is empty ) by A7, A8, WAYBEL_0:def_38;
 ( ( not A2 <> {} & not B2 <> {} ) or B2 <> {} or B1 = {} )
proof
assume  ( A2 <> {} or B2 <> {} ) ; ::_thesis: ( B2 <> {} or B1 = {} )
 ( the carrier of (subrelstr B2) <> {} or the carrier of (subrelstr B1) = {} ) by A8, Th4;
hence  ( B2 <> {} or B1 = {} ) by YELLOW_0:def_15; ::_thesis: verum
end;
then A18: ( the carrier of (subrelstr B2) <> {} or the carrier of (subrelstr B1) = {} ) by A17, YELLOW_0:def_15;
then A19: dom g = the carrier of (subrelstr B1) by FUNCT_2:def_1;
then A20: dom g = B1 by YELLOW_0:def_15;
 ( ( not A1 <> {} & not B1 <> {} ) or A2 <> {} or A1 = {} )
proof
assume  ( A1 <> {} or B1 <> {} ) ; ::_thesis: ( A2 <> {} or A1 = {} )
 ( the carrier of (subrelstr A2) <> {} or the carrier of (subrelstr A1) = {} ) by A7, Th4;
hence  ( A2 <> {} or A1 = {} ) by YELLOW_0:def_15; ::_thesis: verum
end;
then  ( the carrier of (subrelstr A2) <> {} or the carrier of (subrelstr A1) = {} ) by YELLOW_0:def_15;
then  dom f = the carrier of (subrelstr A1) by FUNCT_2:def_1;
then A21: dom f = A1 by YELLOW_0:def_15;
A22: dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def_1;
A23: ( dom f misses dom g implies rng (f +* g) = (rng f) \/ (rng g) )
proof
assume A24: dom f misses dom g ; ::_thesis: rng (f +* g) = (rng f) \/ (rng g)
A25: (rng f) \/ (rng g) c= rng (f +* g)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (rng f) \/ (rng g) or x in rng (f +* g) )
assume A26: x in (rng f) \/ (rng g) ; ::_thesis: x in rng (f +* g)
percases ( x in rng f or x in rng g ) by A26, XBOOLE_0:def_3;
suppose x in rng f ; ::_thesis: x in rng (f +* g)
then consider z being set  such that
A27: z in dom f and
A28: x = f . z by FUNCT_1:def_3;
 not z in dom g by A24, A27, XBOOLE_0:3;
then A29: x = (f +* g) . z by A28, FUNCT_4:11;
 z in dom (f +* g) by A22, A27, XBOOLE_0:def_3;
hence  x in rng (f +* g) by A29, FUNCT_1:def_3; ::_thesis: verum
end;
suppose x in rng g ; ::_thesis: x in rng (f +* g)
then consider z being set  such that
A30: z in dom g and
A31: x = g . z by FUNCT_1:def_3;
 ( z in dom (f +* g) & (f +* g) . z = g . z ) by A22, A30, FUNCT_4:13, XBOOLE_0:def_3;
hence  x in rng (f +* g) by A31, FUNCT_1:def_3; ::_thesis: verum
end;
end;
end;
 rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;
hence  rng (f +* g) = (rng f) \/ (rng g) by A25, XBOOLE_0:def_10; ::_thesis: verum
end;
A32: rng (f +* g) = the carrier of L2
proof
percases ( ( A2 = {} & A1 = {} ) or ( A2 = {} & A1 <> {} ) or ( A2 <> {} & A1 = {} ) or ( A2 <> {} & A1 <> {} ) ) ;
supposeA33: ( A2 = {} & A1 = {} ) ; ::_thesis: rng (f +* g) = the carrier of L2
then  not subrelstr B1 is empty by A2, A16, YELLOW_0:def_15;
then A34: rng g = the carrier of (subrelstr B2) by A8, A17, A33, WAYBEL_0:66, YELLOW_0:def_15;
 rng f = {} by A21, A33, RELAT_1:42;
hence  rng (f +* g) = the carrier of L2 by A5, A21, A23, A33, A34, XBOOLE_1:65, YELLOW_0:def_15; ::_thesis: verum
end;
suppose ( A2 = {} & A1 <> {} ) ; ::_thesis: rng (f +* g) = the carrier of L2
then  ( the carrier of (subrelstr A2) = {} & the carrier of (subrelstr A1) <> {} ) by YELLOW_0:def_15;
hence  rng (f +* g) = the carrier of L2 by A7, Th4; ::_thesis: verum
end;
suppose ( A2 <> {} & A1 = {} ) ; ::_thesis: rng (f +* g) = the carrier of L2
then  ( the carrier of (subrelstr A2) <> {} & the carrier of (subrelstr A1) = {} ) by YELLOW_0:def_15;
hence  rng (f +* g) = the carrier of L2 by A7, Th4; ::_thesis: verum
end;
supposeA35: ( A2 <> {} & A1 <> {} ) ; ::_thesis: rng (f +* g) = the carrier of L2
 rng (f +* g) = the carrier of L2
proof
percases ( B2 <> {} or B2 = {} ) ;
supposeA36: B2 <> {} ; ::_thesis: rng (f +* g) = the carrier of L2
then  the carrier of (subrelstr B2) <> {} by YELLOW_0:def_15;
then  the carrier of (subrelstr B1) <> {} by A8, Th4;
then A37: not subrelstr B1 is empty ;
 ( not subrelstr A2 is empty & not subrelstr A1 is empty ) by A35, YELLOW_0:def_15;
then  rng f = the carrier of (subrelstr A2) by A7, WAYBEL_0:66;
then A38: rng f = A2 by YELLOW_0:def_15;
 not subrelstr B2 is empty by A36, YELLOW_0:def_15;
then  rng g = the carrier of (subrelstr B2) by A8, A37, WAYBEL_0:66;
hence  rng (f +* g) = the carrier of L2 by A1, A5, A21, A20, A23, A38, Th2, YELLOW_0:def_15; ::_thesis: verum
end;
supposeA39: B2 = {} ; ::_thesis: rng (f +* g) = the carrier of L2
 ( not subrelstr A2 is empty & not subrelstr A1 is empty ) by A35, YELLOW_0:def_15;
then A40: rng f = the carrier of (subrelstr A2) by A7, WAYBEL_0:66;
 g = {} by A18, A39, YELLOW_0:def_15;
hence  rng (f +* g) = the carrier of L2 by A5, A23, A39, A40, RELAT_1:38, XBOOLE_1:65, YELLOW_0:def_15; ::_thesis: verum
end;
end;
end;
hence  rng (f +* g) = the carrier of L2 ; ::_thesis: verum
end;
end;
end;
A41: dom (f +* g) = the carrier of L1 by A2, A21, A19, A22, YELLOW_0:def_15;
then A42: for x being set st x in the carrier of L1 holds
(f +* g) . x in the carrier of L2 by A32, FUNCT_1:def_3;
 ( A2 <> {} or B2 <> {} ) by A17, YELLOW_0:def_15;
then reconsider L2 = L2 as non empty RelStr by A5;
reconsider L1 = L1 as non empty RelStr by A16;
reconsider h = f +* g as Function of L1,L2 by A41, A42, FUNCT_2:3;
A43: for x, y being Element of L1 holds
( x <= y iff h . x <= h . y )
proof
let x, y be Element of L1; ::_thesis: ( x <= y iff h . x <= h . y )
A44: dom f misses dom g by A6, A21, A19, YELLOW_0:def_15;
percases ( ( x in A1 & y in A1 ) or ( x in A1 & y in B1 ) or ( x in B1 & y in A1 ) or ( x in B1 & y in B1 ) ) by A2, XBOOLE_0:def_3;
supposeA45: ( x in A1 & y in A1 ) ; ::_thesis: ( x <= y iff h . x <= h . y )
then  the carrier of (subrelstr A2) <> {} by A7, Th4;
then reconsider A29 = A2 as non empty Subset of L2 by YELLOW_0:def_15;
reconsider A19 = A1 as non empty Subset of L1 by A45;
reconsider ax = x, ay = y as Element of (subrelstr A19) by A45, YELLOW_0:def_15;
reconsider f9 = f as Function of (subrelstr A19),(subrelstr A29) ;
A46: ( h . x = f . x & h . y = f . y ) by A1, A21, A20, A45, Th2, FUNCT_4:16;
hereby  ::_thesis: ( h . x <= h . y implies x <= y )
assume  x <= y ; ::_thesis: h . x <= h . y
then  ax <= ay by YELLOW_0:60;
then  f9 . ax <= f9 . ay by A7, WAYBEL_0:66;
hence  h . x <= h . y by A46, YELLOW_0:59; ::_thesis: verum
end;
assume  h . x <= h . y ; ::_thesis: x <= y
then  f9 . ax <= f9 . ay by A46, YELLOW_0:60;
then  ax <= ay by A7, WAYBEL_0:66;
hence  x <= y by YELLOW_0:59; ::_thesis: verum
end;
supposeA47: ( x in A1 & y in B1 ) ; ::_thesis: ( x <= y iff h . x <= h . y )
hereby  ::_thesis: ( h . x <= h . y implies x <= y )
 ( the carrier of (subrelstr A2) <> {} & the carrier of (subrelstr B2) <> {} ) by A7, A8, A47, Th4;
then reconsider A29 = A2, B29 = B2 as non empty Subset of L2 by YELLOW_0:def_15;
reconsider A19 = A1, B19 = B1 as non empty Subset of L1 by A47;
assume  x <= y ; ::_thesis: h . x <= h . y
reconsider f9 = f as Function of (subrelstr A19),(subrelstr A29) ;
reconsider g9 = g as Function of (subrelstr B19),(subrelstr B29) ;
reconsider ax = x as Element of (subrelstr A19) by A47, YELLOW_0:def_15;
reconsider ay = y as Element of (subrelstr B19) by A47, YELLOW_0:def_15;
 f9 . ax in the carrier of (subrelstr A29) ;
then A48: f9 . ax in A29 by YELLOW_0:def_15;
 g9 . ay in the carrier of (subrelstr B29) ;
then A49: g9 . ay in B29 by YELLOW_0:def_15;
 ( f . x = h . x & g . y = h . y ) by A21, A20, A44, A47, FUNCT_4:13, FUNCT_4:16;
then  h . x < h . y by A3, A48, A49, Def3;
hence  h . x <= h . y by ORDERS_2:def_6; ::_thesis: verum
end;
assume  h . x <= h . y ; ::_thesis: x <= y
 x < y by A1, A47, Def3;
hence  x <= y by ORDERS_2:def_6; ::_thesis: verum
end;
supposeA50: ( x in B1 & y in A1 ) ; ::_thesis: ( x <= y iff h . x <= h . y )
then  not the carrier of (subrelstr B2) is empty by A8, Th4;
then  not subrelstr B2 is empty ;
then A51: rng g = the carrier of (subrelstr B2) by A8, A50, WAYBEL_0:66;
 g . x in rng g by A20, A50, FUNCT_1:def_3;
then A52: g . x in B2 by A51, YELLOW_0:def_15;
 not the carrier of (subrelstr A2) is empty by A7, A50, Th4;
then  not subrelstr A2 is empty ;
then A53: rng f = the carrier of (subrelstr A2) by A7, A50, WAYBEL_0:66;
 f . y in rng f by A21, A50, FUNCT_1:def_3;
then A54: f . y in A2 by A53, YELLOW_0:def_15;
 y < x by A1, A50, Def3;
hence  ( x <= y implies h . x <= h . y ) by ORDERS_2:6; ::_thesis: ( h . x <= h . y implies x <= y )
assume A55: h . x <= h . y ; ::_thesis: x <= y
 ( g . x = h . x & f . y = h . y ) by A1, A21, A20, A50, Th2, FUNCT_4:13, FUNCT_4:16;
then  h . x > h . y by A3, A52, A54, Def3;
hence  x <= y by A55, ORDERS_2:6; ::_thesis: verum
end;
supposeA56: ( x in B1 & y in B1 ) ; ::_thesis: ( x <= y iff h . x <= h . y )
then  the carrier of (subrelstr B2) <> {} by A8, Th4;
then reconsider B29 = B2 as non empty Subset of L2 by YELLOW_0:def_15;
reconsider B19 = B1 as non empty Subset of L1 by A56;
reconsider ax = x, ay = y as Element of (subrelstr B19) by A56, YELLOW_0:def_15;
reconsider g9 = g as Function of (subrelstr B19),(subrelstr B29) ;
A57: ( h . x = g . x & h . y = g . y ) by A20, A56, FUNCT_4:13;
hereby  ::_thesis: ( h . x <= h . y implies x <= y )
assume  x <= y ; ::_thesis: h . x <= h . y
then  ax <= ay by YELLOW_0:60;
then  g9 . ax <= g9 . ay by A8, WAYBEL_0:66;
hence  h . x <= h . y by A57, YELLOW_0:59; ::_thesis: verum
end;
assume  h . x <= h . y ; ::_thesis: x <= y
then  g9 . ax <= g9 . ay by A57, YELLOW_0:60;
then  ax <= ay by A8, WAYBEL_0:66;
hence  x <= y by YELLOW_0:59; ::_thesis: verum
end;
end;
end;
 h is V13()
proof
let x1, x2 be Element of L1; :: according to WAYBEL_1:def_1 ::_thesis: ( not h . x1 = h . x2 or x1 = x2 )
assume A58: h . x1 = h . x2 ; ::_thesis: x1 = x2
percases ( ( x1 in A1 & x2 in A1 ) or ( x1 in A1 & x2 in B1 ) or ( x1 in B1 & x2 in A1 ) or ( x1 in B1 & x2 in B1 ) ) by A2, XBOOLE_0:def_3;
supposeA59: ( x1 in A1 & x2 in A1 ) ; ::_thesis: x1 = x2
then  not x1 in B1 by A6, XBOOLE_0:3;
then A60: h . x1 = f . x1 by A20, FUNCT_4:11;
 the carrier of (subrelstr A2) <> {} by A7, A59, Th4;
then A61: not subrelstr A2 is empty ;
 not x2 in B1 by A6, A59, XBOOLE_0:3;
then  f . x1 = f . x2 by A20, A58, A60, FUNCT_4:11;
hence  x1 = x2 by A7, A21, A59, A61, FUNCT_1:def_4; ::_thesis: verum
end;
supposeA62: ( x1 in A1 & x2 in B1 ) ; ::_thesis: x1 = x2
then  the carrier of (subrelstr A2) <> {} by A7, Th4;
then  not subrelstr A2 is empty ;
then  rng f = the carrier of (subrelstr A2) by A7, A62, WAYBEL_0:66;
then A63: rng f = A2 by YELLOW_0:def_15;
 not x1 in B1 by A6, A62, XBOOLE_0:3;
then  h . x2 = f . x1 by A20, A58, FUNCT_4:11;
then A64: h . x2 in rng f by A21, A62, FUNCT_1:def_3;
 h . x2 = g . x2 by A20, A62, FUNCT_4:13;
then A65: h . x2 in rng g by A20, A62, FUNCT_1:def_3;
 the carrier of (subrelstr B2) <> {} by A8, A62, Th4;
then  not subrelstr B2 is empty ;
then  rng g = the carrier of (subrelstr B2) by A8, A62, WAYBEL_0:66;
then  rng f misses rng g by A4, A63, YELLOW_0:def_15;
hence  x1 = x2 by A64, A65, XBOOLE_0:3; ::_thesis: verum
end;
supposeA66: ( x1 in B1 & x2 in A1 ) ; ::_thesis: x1 = x2
then  not x2 in dom g by A6, A20, XBOOLE_0:3;
then  h . x2 = f . x2 by FUNCT_4:11;
then A67: h . x2 in rng f by A21, A66, FUNCT_1:def_3;
 the carrier of (subrelstr B2) <> {} by A8, A66, Th4;
then  not subrelstr B2 is empty ;
then A68: rng g = the carrier of (subrelstr B2) by A8, A66, WAYBEL_0:66;
 h . x2 = g . x1 by A20, A58, A66, FUNCT_4:13;
then A69: h . x2 in rng g by A20, A66, FUNCT_1:def_3;
 the carrier of (subrelstr A2) <> {} by A7, A66, Th4;
then  not subrelstr A2 is empty ;
then  rng f = the carrier of (subrelstr A2) by A7, A66, WAYBEL_0:66
.= A2 by YELLOW_0:def_15 ;
then  rng f misses rng g by A4, A68, YELLOW_0:def_15;
hence  x1 = x2 by A69, A67, XBOOLE_0:3; ::_thesis: verum
end;
supposeA70: ( x1 in B1 & x2 in B1 ) ; ::_thesis: x1 = x2
then  the carrier of (subrelstr B2) <> {} by A8, Th4;
then A71: not subrelstr B2 is empty ;
 h . x1 = g . x1 by A20, A70, FUNCT_4:13;
then  g . x1 = g . x2 by A20, A58, A70, FUNCT_4:13;
hence  x1 = x2 by A8, A20, A70, A71, FUNCT_1:def_4; ::_thesis: verum
end;
end;
end;
then  h is isomorphic by A32, A43, WAYBEL_0:66;
hence  ex h being Function of L1,L2 st
( h = f +* g & h is isomorphic ) ; ::_thesis: verum
end;
end;
end;

theorem :: ORDERS_4:6
for A being finite Chain
for n being Nat st card the carrier of A = n holds
A, InclPoset n are_isomorphic
proof
defpred S1[ 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 S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: for A being finite Chain st card the carrier of A = n holds
A, InclPoset n are_isomorphic ; ::_thesis: S1[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;
percases ( n + 1 = 1 or n + 1 > 1 ) by A3, NAT_1:13;
supposeA5: n + 1 = 1 ; ::_thesis: A, InclPoset (n + 1) are_isomorphic
then consider x being set  such that
A6: the carrier of A = {x} by A4, CARD_2:42;
 A, InclPoset 1 are_isomorphic
proof
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 )
proof
let e, f be Element of A; ::_thesis: ( e <= f iff g . e <= g . f )
hereby  ::_thesis: ( g . e <= g . f implies e <= f )
assume  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;
assume  g . e <= g . f ; ::_thesis: e <= f
 e = x by A6, TARSKI:def_1;
hence  e <= f by A6, TARSKI:def_1; ::_thesis: verum
end;
 g is V13()
proof
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;
then  g is isomorphic by A7, A8, A9, WAYBEL_0:66;
hence  A, InclPoset 1 are_isomorphic by WAYBEL_1:def_8; ::_thesis: verum
end;
hence  A, InclPoset (n + 1) are_isomorphic by A5; ::_thesis: verum
end;
supposeA10: 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 by WAYBEL_1:def_8;
 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: n + 1 = succ n by NAT_1:38
.= n \/ {n} by ORDINAL1:def_1 ;
then  {n} c= 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
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 Element of NAT : i < n  }  by AXIOMS:4;
then consider h being Element of NAT  such that
A20: h = a and
A21: h < n ;
A22: b = n by A18, TARSKI:def_1;
 a c= b
proof
assume  not a c= b ; ::_thesis: contradiction
then consider x being set  such that
A23: x in a and
A24: not x in b by TARSKI:def_3;
 x in  {  w where w is Element of NAT : w < h  }  by A20, A23, AXIOMS:4;
then consider w9 being Element of 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 Element of NAT : t < n  }  ;
hence  contradiction by A22, A24, A25, AXIOMS:4; ::_thesis: verum
end;
then A27: a <= b by YELLOW_1:3;
 a <> b by A19, A22;
hence  a < b by A27, ORDERS_2:def_6; ::_thesis: verum
end;
 the carrier of (InclPoset n) = n by YELLOW_1:1;
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, Def3;
 n <= n + 1 by NAT_1:11;
then  n c= 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
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;
hereby  ::_thesis: ( g . e <= g . f implies e <= f )
assume  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;
assume  g . e <= g . f ; ::_thesis: e <= f
 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;
 g is V13() by A29, PARTFUN1:17;
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 by WAYBEL_1:def_8; ::_thesis: verum
end;
end;
end;
A36: S1[ 0 ]
proof
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;
 for n being Nat holds S1[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
end;