:: 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;