:: The Class of Series-Parallel Graphs, {III}
:: by Krzysztof Retel
::
:: Received February 3, 2004
:: Copyright (c) 2004-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, RELAT_1, XBOOLE_0, ZFMISC_1, TARSKI, RELAT_2, STRUCT_0,
FINSET_1, ORDERS_2, CARD_1, CAT_1, YELLOW_0, WELLORD1, NECKLA_2,
NECKLACE, SUBSET_1, FUNCT_1, XXREAL_0, SEQM_3, REWRITE1, FINSEQ_1, NAT_1,
ARYTM_3, FINSEQ_5, EQREL_1, MSUALG_5, CLASSES2, FUNCOP_1, FUNCT_4,
ARYTM_1, NECKLA_3, XCMPLX_0;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ZFMISC_1, RELAT_1, RELAT_2,
RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSET_1, ORDINAL1, CARD_1,
NUMBERS, XCMPLX_0, XXREAL_0, DOMAIN_1, STRUCT_0, ORDERS_2, WAYBEL_1,
FUNCOP_1, CLASSES2, NECKLACE, WAYBEL_0, FUNCT_4, REWRITE1, FINSEQ_1,
FINSEQ_5, EQREL_1, MSUALG_5, YELLOW_0, NECKLA_2, WELLORD1;
constructors NAT_1, EQREL_1, CLASSES1, TOLER_1, CLASSES2, FINSEQ_5, REWRITE1,
REALSET2, MSUALG_5, ORDERS_3, WAYBEL_1, NECKLACE, NECKLA_2, RELSET_1,
FUNCT_4;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
FUNCOP_1, FINSET_1, XXREAL_0, XREAL_0, NAT_1, CARD_1, FINSEQ_1, STRUCT_0,
ORDERS_2, YELLOW_0, NECKLACE, NECKLA_2, ORDINAL1, FUNCT_4, RELSET_1,
ZFMISC_1;
requirements BOOLE, SUBSET, REAL, NUMERALS, ARITHM;
definitions XBOOLE_0, TARSKI, NECKLACE, RELAT_2;
equalities TARSKI, FUNCOP_1, WELLORD1, STRUCT_0, ORDINAL1;
expansions XBOOLE_0, TARSKI, NECKLACE, RELAT_2;
theorems RELSET_1, NECKLACE, XBOOLE_0, WAYBEL_0, YELLOW_0, FUNCT_1, FUNCT_2,
ORDERS_2, RELAT_2, SUBSET_1, ZFMISC_1, XBOOLE_1, TARSKI, MCART_1,
CLASSES2, CLASSES1, NECKLA_2, FUNCOP_1, ENUMSET1, RELAT_1, SYSREL,
PARTFUN1, GROUP_6, CARD_2, REWRITE1, FINSEQ_1, FINSEQ_3, FINSEQ_5, NAT_1,
EQREL_1, MSUALG_6, MSUALG_5, CARD_1, NAT_2, FUNCT_4, FUNCT_3, WAYBEL_1,
YELLOW_6, XREAL_1, XXREAL_0, ORDINAL1, NAT_D, STRUCT_0, XTUPLE_0;
schemes NAT_1;
begin :: Preliminaries
reserve A,B,a,b,c,d,e,f,g,h for set;
theorem Th1:
(id A)|B = id A /\ [:B,B:]
proof
thus (id A)|B c= id A /\ [:B,B:]
proof
let a be object;
assume
A1: a in (id A)|B;
(id A)|B is Relation of B,A by RELSET_1:18;
then consider x,y being object such that
A2: a = [x,y] and
A3: x in B and
y in A by A1,RELSET_1:2;
A4: [x,y] in id A by A1,A2,RELAT_1:def 11;
then x = y by RELAT_1:def 10;
then [x,y] in [:B,B:] by A3,ZFMISC_1:87;
hence thesis by A2,A4,XBOOLE_0:def 4;
end;
let a be object;
assume
A5: a in id A /\ [:B,B:];
then a in [:B,B:] by XBOOLE_0:def 4;
then
A6: ex x1,y1 being object st x1 in B & y1 in B & a = [x1,y1]
by ZFMISC_1:def 2;
a in id A by A5,XBOOLE_0:def 4;
hence thesis by A6,RELAT_1:def 11;
end;
theorem
id {a,b,c,d} = {[a,a],[b,b],[c,c],[d,d]}
proof
set X = {a,b,c,d};
thus id X c= {[a,a],[b,b],[c,c],[d,d]}
proof
let x be object;
assume
A1: x in id X;
then consider x1,y1 being object such that
A2: x = [x1,y1] and
A3: x1 in X and
y1 in X by RELSET_1:2;
A4: x1 = y1 by A1,A2,RELAT_1:def 10;
per cases by A3,ENUMSET1:def 2;
suppose
x1 = a;
hence thesis by A2,A4,ENUMSET1:def 2;
end;
suppose
x1 = b;
hence thesis by A2,A4,ENUMSET1:def 2;
end;
suppose
x1 = c;
hence thesis by A2,A4,ENUMSET1:def 2;
end;
suppose
x1 = d;
hence thesis by A2,A4,ENUMSET1:def 2;
end;
end;
let x be object;
assume
A5: x in {[a,a],[b,b],[c,c],[d,d]};
per cases by A5,ENUMSET1:def 2;
suppose
A6: x = [a,a];
a in X by ENUMSET1:def 2;
hence thesis by A6,RELAT_1:def 10;
end;
suppose
A7: x = [b,b];
b in X by ENUMSET1:def 2;
hence thesis by A7,RELAT_1:def 10;
end;
suppose
A8: x = [c,c];
c in X by ENUMSET1:def 2;
hence thesis by A8,RELAT_1:def 10;
end;
suppose
A9: x = [d,d];
d in X by ENUMSET1:def 2;
hence thesis by A9,RELAT_1:def 10;
end;
end;
theorem Th3:
[:{a,b,c,d},{e,f,g,h}:] = {[a,e],[a,f],[b,e],[b,f],[a,g],[a,h],[b
,g],[b,h]} \/ {[c,e],[c,f],[d,e],[d,f],[c,g],[c,h],[d,g],[d,h]}
proof
set X1 = {a,b,c,d}, Y1 = {e,f,g,h}, X11 = {a,b}, X12 = {c,d}, Y11 = {e,f},
Y12 = {g,h};
A1: [:X12,Y11:] = {[c,e],[c,f],[d,e],[d,f]} & [:X12,Y12:] = {[c,g],[c,h],[d,
g],[ d,h]} by MCART_1:23;
X1 = X11 \/ X12 & Y1 = Y11 \/ Y12 by ENUMSET1:5;
then
A2: [:X1,Y1:] = [:X11,Y11:] \/ [:X11,Y12:] \/ [:X12,Y11:] \/ [:X12,Y12:] by
ZFMISC_1:98;
[:X11,Y11:] = {[a,e],[a,f],[b,e],[b,f]} & [:X11,Y12:] = {[a,g],[a,h],[b,
g],[ b,h]} by MCART_1:23;
then
[:X1,Y1:] = {[a,e],[a,f],[b,e],[b,f],[a,g],[a,h],[b,g],[b,h]} \/ {[c,e],
[c,f],[d,e],[d,f]} \/ {[c,g],[c,h],[d,g],[d,h]} by A1,A2,ENUMSET1:25
.= {[a,e],[a,f],[b,e],[b,f],[a,g],[a,h],[b,g],[b,h]} \/ ({[c,e],[c,f],[d
,e],[d,f]} \/ {[c,g],[c,h],[d,g],[d,h]}) by XBOOLE_1:4
.= {[a,e],[a,f],[b,e],[b,f],[a,g],[a,h],[b,g],[b,h]} \/ {[c,e],[c,f],[d,
e],[d,f],[c,g],[c,h],[d,g],[d,h]} by ENUMSET1:25;
hence thesis;
end;
registration
let X,Y be trivial set;
cluster -> trivial for Relation of X,Y;
correctness;
end;
theorem Th4:
for X be trivial set, R be Relation of X st R is non empty holds
ex x be object st R = {[x,x]}
proof
let X be trivial set;
let R be Relation of X;
assume R is non empty;
then consider x be object such that
A1: x in R;
consider y,z be object such that
A2: x = [y,z] and
A3: y in X and
A4: z in X by A1,RELSET_1:2;
consider a be object such that
A5: X = {a} by A3,ZFMISC_1:131;
A6: y = a & z = a by A3,A4,A5,TARSKI:def 1;
R = {[a,a]}
proof
thus R c= {[a,a]}
proof
let r be object;
assume r in R;
then consider y,z be object such that
A7: r = [y,z] and
A8: y in X & z in X by RELSET_1:2;
y = a & z = a by A5,A8,TARSKI:def 1;
hence thesis by A7,TARSKI:def 1;
end;
let z be object;
assume z in {[a,a]};
hence thesis by A1,A2,A6,TARSKI:def 1;
end;
hence thesis;
end;
registration
let X be trivial set;
cluster -> trivial reflexive symmetric transitive strongly_connected
for Relation of X;
correctness
proof
let R be Relation of X,X;
A1: R is_reflexive_in field R
proof
per cases;
suppose
A2: R is empty;
let x be object;
assume x in field R;
hence thesis by A2,RELAT_1:40;
end;
suppose
R is non empty;
then consider z be object such that
A3: R = {[z,z]} by Th4;
let x be object;
assume x in field R;
then
A4: x in dom R \/ rng R by RELAT_1:def 6;
dom R = {z} & rng R = {z} by A3,RELAT_1:9;
then x = z by A4,TARSKI:def 1;
hence thesis by A3,TARSKI:def 1;
end;
end;
A5: R is_transitive_in field R
proof
per cases;
suppose
A6: R is empty;
let x,y,z be object;
assume that
x in field R and
y in field R and
z in field R and
A7: [x,y] in R and
[y,z] in R;
thus thesis by A6,A7;
end;
suppose
A8: R is non empty;
let x,y,z be object;
assume that
x in field R and
y in field R and
z in field R and
A9: [x,y] in R and
A10: [y,z] in R;
consider a be object such that
A11: R = {[a,a]} by A8,Th4;
[y,z] = [a,a] by A11,A10,TARSKI:def 1;
then
A12: z = a by XTUPLE_0:1;
[x,y] = [a,a] by A11,A9,TARSKI:def 1;
then x = a by XTUPLE_0:1;
hence thesis by A11,A12,TARSKI:def 1;
end;
end;
A13: R is_strongly_connected_in field R
proof
per cases;
suppose
A14: R is empty;
let x,y be object;
assume that
A15: x in field R and
y in field R;
thus thesis by A14,A15,RELAT_1:40;
end;
suppose
A16: R is non empty;
let x,y be object;
assume that
A17: x in field R and
A18: y in field R;
consider a be object such that
A19: R = {[a,a]} by A16,Th4;
A20: dom R = {a} & rng R = {a} by A19,RELAT_1:9;
y in dom R \/ rng R by A18,RELAT_1:def 6;
then
A21: y = a by A20,TARSKI:def 1;
x in dom R \/ rng R by A17,RELAT_1:def 6;
then x = a by A20,TARSKI:def 1;
hence thesis by A19,A21,TARSKI:def 1;
end;
end;
R is_symmetric_in field R
proof
per cases;
suppose
A22: R is empty;
let x,y be object;
assume that
x in field R and
y in field R and
A23: [x,y] in R;
thus thesis by A22,A23;
end;
suppose
A24: R is non empty;
let x,y be object;
assume that
x in field R and
y in field R and
A25: [x,y] in R;
consider a be object such that
A26: R = {[a,a]} by A24,Th4;
[x,y] = [a,a] by A26,A25,TARSKI:def 1;
then x = a & y = a by XTUPLE_0:1;
hence thesis by A26,TARSKI:def 1;
end;
end;
hence thesis by A1,A5,A13;
end;
end;
theorem Th5:
for X be 1-element set, R be Relation of X holds R is_symmetric_in X
proof
let X be 1-element set;
let R be Relation of X;
consider x be object such that
A1: X = {x} by ZFMISC_1:131;
let a,b be object;
assume that
A2: a in X and
A3: b in X & [a,b] in R;
a = x by A1,A2,TARSKI:def 1;
hence thesis by A1,A3,TARSKI:def 1;
end;
registration
cluster non empty strict finite irreflexive symmetric for RelStr;
correctness
proof
set X = {0,1}, r = {[0,1],[1,0]};
0 in X & 1 in X by TARSKI:def 2;
then
A1: [0,1] in [:X,X:] & [1,0] in [:X,X:] by ZFMISC_1:def 2;
r c= [:X,X:]
by A1,TARSKI:def 2;
then reconsider r as Relation of X,X;
take R = RelStr (#X,r#);
A2: for x being set st x in the carrier of R holds not [x,x] in the
InternalRel of R
proof
let x be set;
A3: not [0,0] in r
proof
assume [0,0] in r;
then [0,0] = [0,1] or [0,0] = [1,0] by TARSKI:def 2;
hence contradiction by XTUPLE_0:1;
end;
A4: not [1,1] in r
proof
assume [1,1] in r;
then [1,1] = [0,1] or [1,1] = [1,0] by TARSKI:def 2;
hence contradiction by XTUPLE_0:1;
end;
assume x in the carrier of R;
then x = 0 or x = 1 by TARSKI:def 2;
hence thesis by A3,A4;
end;
for x,y be object st x in X & y in X & [x,y] in r holds [y,x] in r
proof
let x,y be object;
assume that
x in X and
y in X and
A5: [x,y] in r;
per cases by A5,TARSKI:def 2;
suppose
[x,y] = [0,1];
then x = 0 & y = 1 by XTUPLE_0:1;
hence thesis by TARSKI:def 2;
end;
suppose
[x,y] = [1,0];
then x = 1 & y = 0 by XTUPLE_0:1;
hence thesis by TARSKI:def 2;
end;
end;
then r is_symmetric_in X;
hence thesis by A2;
end;
end;
registration
let L be irreflexive RelStr;
cluster -> irreflexive for full SubRelStr of L;
correctness
proof
let S be full SubRelStr of L;
let x be set;
assume
A1: x in the carrier of S;
the carrier of S c= the carrier of L by YELLOW_0:def 13;
then the InternalRel of S = (the InternalRel of L) |_2 the carrier of S &
not [x, x] in the InternalRel of L by A1,NECKLACE:def 5,YELLOW_0:def 14;
hence thesis by XBOOLE_0:def 4;
end;
end;
registration
let L be symmetric RelStr;
cluster -> symmetric for full SubRelStr of L;
correctness
proof
let S be full SubRelStr of L;
let x,y be object;
assume that
A1: x in the carrier of S & y in the carrier of S and
A2: [x,y] in the InternalRel of S;
A3: [y,x] in [:the carrier of S,the carrier of S:] by A1,ZFMISC_1:87;
A4: the carrier of S c= the carrier of L & the InternalRel of L
is_symmetric_in the carrier of L by NECKLACE:def 3,YELLOW_0:def 13;
A5: the InternalRel of S = (the InternalRel of L) |_2 the carrier of S by
YELLOW_0:def 14;
then [x,y] in the InternalRel of L by A2,XBOOLE_0:def 4;
then [y,x] in the InternalRel of L by A1,A4;
hence thesis by A5,A3,XBOOLE_0:def 4;
end;
end;
theorem Th6:
for R be irreflexive symmetric RelStr st card (the carrier of R) = 2
ex a,b be object st the carrier of R = {a,b} & (the InternalRel of R = {
[a,b],[b,a]} or the InternalRel of R = {})
proof
let R be irreflexive symmetric RelStr;
set Q = the InternalRel of R;
assume
A1: card (the carrier of R) = 2;
then reconsider X = the carrier of R as finite set;
consider a,b be object such that
A2: a <> b and
A3: X = {a,b} by A1,CARD_2:60;
A4: the InternalRel of R c= {[a,b],[b,a]}
proof
let x be object;
assume
A5: x in the InternalRel of R;
then consider x1,x2 be object such that
A6: x = [x1,x2] and
A7: x1 in X and
A8: x2 in X by RELSET_1:2;
A9: x1 = a or x1 = b by A3,A7,TARSKI:def 2;
per cases by A3,A6,A8,A9,TARSKI:def 2;
suppose
A10: x = [a,a];
a in the carrier of R by A3,TARSKI:def 2;
hence thesis by A5,A10,NECKLACE:def 5;
end;
suppose
x = [a,b];
hence thesis by TARSKI:def 2;
end;
suppose
x = [b,a];
hence thesis by TARSKI:def 2;
end;
suppose
A11: x = [b,b];
b in the carrier of R by A3,TARSKI:def 2;
hence thesis by A5,A11,NECKLACE:def 5;
end;
end;
per cases by A4,ZFMISC_1:36;
suppose
Q = {};
hence thesis by A3;
end;
suppose
A12: Q = {[a,b]};
A13: a in X & b in X by A3,TARSKI:def 2;
A14: Q is_symmetric_in X by NECKLACE:def 3;
[a,b] in Q by A12,TARSKI:def 1;
then [b,a] in Q by A13,A14;
then [b,a] = [a,b] by A12,TARSKI:def 1;
hence thesis by A2,XTUPLE_0:1;
end;
suppose
A15: Q = {[b,a]};
A16: a in X & b in X by A3,TARSKI:def 2;
A17: Q is_symmetric_in X by NECKLACE:def 3;
[b,a] in Q by A15,TARSKI:def 1;
then [a,b] in Q by A16,A17;
then [b,a] = [a,b] by A15,TARSKI:def 1;
hence thesis by A2,XTUPLE_0:1;
end;
suppose
Q = {[a,b],[b,a]};
hence thesis by A3;
end;
end;
begin :: Some facts about operations 'union_of' and 'sum_of'
registration
let R be non empty RelStr,S be RelStr;
cluster union_of(R,S) -> non empty;
correctness
proof
(the carrier of R) \/ (the carrier of S) is non empty;
hence thesis by NECKLA_2:def 2;
end;
cluster sum_of(R,S) -> non empty;
correctness
proof
(the carrier of R) \/ (the carrier of S) is non empty;
hence thesis by NECKLA_2:def 3;
end;
end;
registration
let R be RelStr, S be non empty RelStr;
cluster union_of(R,S) -> non empty;
correctness
proof
(the carrier of R) \/ (the carrier of S) is non empty;
hence thesis by NECKLA_2:def 2;
end;
cluster sum_of(R,S) -> non empty;
correctness
proof
(the carrier of R) \/ (the carrier of S) is non empty;
hence thesis by NECKLA_2:def 3;
end;
end;
registration
let R,S be finite RelStr;
cluster union_of(R,S) -> finite;
correctness
proof
(the carrier of R) \/ the carrier of S is finite;
hence thesis by NECKLA_2:def 2;
end;
cluster sum_of(R,S) -> finite;
correctness
proof
(the carrier of R) \/ the carrier of S is finite;
hence thesis by NECKLA_2:def 3;
end;
end;
registration
let R,S be symmetric RelStr;
cluster union_of(R,S) -> symmetric;
correctness
proof
let x,y be object;
set U = union_of(R,S), cU = the carrier of U, IU = the InternalRel of U,
cR = the carrier of R, cS = the carrier of S;
assume that
x in cU and
y in cU and
A1: [x,y] in IU;
A2: [x,y] in (the InternalRel of R) \/ the InternalRel of S by A1,
NECKLA_2:def 2;
per cases by A2,XBOOLE_0:def 3;
suppose
A3: [x,y] in the InternalRel of R;
A4: the InternalRel of R is_symmetric_in cR by NECKLACE:def 3;
x in cR & y in cR by A3,ZFMISC_1:87;
then [y,x] in the InternalRel of R by A3,A4;
then [y,x] in (the InternalRel of R) \/ the InternalRel of S by
XBOOLE_0:def 3;
hence thesis by NECKLA_2:def 2;
end;
suppose
A5: [x,y] in the InternalRel of S;
A6: the InternalRel of S is_symmetric_in cS by NECKLACE:def 3;
x in cS & y in cS by A5,ZFMISC_1:87;
then [y,x] in the InternalRel of S by A5,A6;
then [y,x] in (the InternalRel of R) \/ the InternalRel of S by
XBOOLE_0:def 3;
hence thesis by NECKLA_2:def 2;
end;
end;
cluster sum_of(R,S) -> symmetric;
correctness
proof
set SU = sum_of(R,S), cSU = the carrier of sum_of(R,S), ISU = the
InternalRel of SU, cR = the carrier of R, IR = the InternalRel of R, cS = the
carrier of S, IS = the InternalRel of S;
A7: IS is_symmetric_in cS by NECKLACE:def 3;
A8: IR is_symmetric_in cR by NECKLACE:def 3;
the InternalRel of sum_of(R,S) is_symmetric_in cSU
proof
let x,y be object;
assume that
x in cSU and
y in cSU and
A9: [x,y] in ISU;
[x,y] in IR \/ IS \/ [:cR,cS:] \/ [:cS,cR:] by A9,NECKLA_2:def 3;
then [x,y] in IR \/ IS \/ [:cR,cS:] or [x,y] in [:cS,cR:] by
XBOOLE_0:def 3;
then
A10: [x,y] in IR \/ IS or [x,y] in [:cR,cS:] or [x,y] in [:cS, cR:] by
XBOOLE_0:def 3;
per cases by A10,XBOOLE_0:def 3;
suppose
A11: [x,y] in IR;
then x in cR & y in cR by ZFMISC_1:87;
then [y,x] in IR by A8,A11;
then [y,x] in IR \/ IS by XBOOLE_0:def 3;
then [y,x] in IR \/ IS \/ [:cR,cS:] by XBOOLE_0:def 3;
then [y,x] in IR \/ IS \/ [:cR,cS:] \/ [:cS,cR:] by XBOOLE_0:def 3;
hence thesis by NECKLA_2:def 3;
end;
suppose
A12: [x,y] in IS;
then x in cS & y in cS by ZFMISC_1:87;
then [y,x] in IS by A7,A12;
then [y,x] in IR \/ IS by XBOOLE_0:def 3;
then [y,x] in IR \/ IS \/ [:cR,cS:] by XBOOLE_0:def 3;
then [y,x] in IR \/ IS \/ [:cR,cS:] \/ [:cS,cR:] by XBOOLE_0:def 3;
hence thesis by NECKLA_2:def 3;
end;
suppose
[x,y] in [:cR,cS:];
then x in cR & y in cS by ZFMISC_1:87;
then [y,x] in [:cS,cR:] by ZFMISC_1:87;
then [y,x] in [:cR,cS:] \/ [:cS,cR:] by XBOOLE_0:def 3;
then [y,x] in IS \/ ([:cR,cS:] \/ [:cS,cR:]) by XBOOLE_0:def 3;
then [y,x] in IS \/ [:cR,cS:] \/ [:cS,cR:] by XBOOLE_1:4;
then [y,x] in IR \/ (IS \/ [:cR,cS:] \/ [:cS,cR:]) by XBOOLE_0:def 3;
then [y,x] in IR \/ (IS \/ ([:cR,cS:] \/ [:cS,cR:])) by XBOOLE_1:4;
then [y,x] in IR \/ IS \/ ([:cR,cS:] \/ [:cS,cR:]) by XBOOLE_1:4;
then [y,x] in IR \/ IS \/ [:cR,cS:] \/ [:cS,cR:] by XBOOLE_1:4;
hence thesis by NECKLA_2:def 3;
end;
suppose
[x,y] in [:cS,cR:];
then x in cS & y in cR by ZFMISC_1:87;
then [y,x] in [:cR,cS:] by ZFMISC_1:87;
then [y,x] in [:cR,cS:] \/ [:cS,cR:] by XBOOLE_0:def 3;
then [y,x] in IS \/ ([:cR,cS:] \/ [:cS,cR:]) by XBOOLE_0:def 3;
then [y,x] in IS \/ [:cR,cS:] \/ [:cS,cR:] by XBOOLE_1:4;
then [y,x] in IR \/ (IS \/ [:cR,cS:] \/ [:cS,cR:]) by XBOOLE_0:def 3;
then [y,x] in IR \/ (IS \/ ([:cR,cS:] \/ [:cS,cR:])) by XBOOLE_1:4;
then [y,x] in IR \/ IS \/ ([:cR,cS:] \/ [:cS,cR:]) by XBOOLE_1:4;
then [y,x] in IR \/ IS \/ [:cR,cS:] \/ [:cS,cR:] by XBOOLE_1:4;
hence thesis by NECKLA_2:def 3;
end;
end;
hence thesis;
end;
end;
registration
let R,S be irreflexive RelStr;
cluster union_of(R,S) -> irreflexive;
correctness
proof
set U = union_of(R,S), cU = the carrier of U, IU = the InternalRel of U,
cR = the carrier of R, cS = the carrier of S;
for x be set st x in cU holds not [x,x] in IU
proof
let x be set such that
x in cU;
assume not thesis;
then
A1: [x,x] in (the InternalRel of R) \/ the InternalRel of S by NECKLA_2:def 2
;
per cases by A1,XBOOLE_0:def 3;
suppose
A2: [x,x] in the InternalRel of R;
then x in cR by ZFMISC_1:87;
hence thesis by A2,NECKLACE:def 5;
end;
suppose
A3: [x,x] in the InternalRel of S;
then x in cS by ZFMISC_1:87;
hence thesis by A3,NECKLACE:def 5;
end;
end;
hence thesis;
end;
end;
theorem
for R,S be irreflexive RelStr st the carrier of R misses the carrier
of S holds sum_of(R,S) is irreflexive
proof
let R,S be irreflexive RelStr such that
A1: the carrier of R misses the carrier of S;
for x be set st x in the carrier of sum_of(R,S) holds not [x,x] in the
InternalRel of sum_of(R,S)
proof
set IR = the InternalRel of R, IS = the InternalRel of S, RS = [:the
carrier of R,the carrier of S:], SR = [:the carrier of S,the carrier of R:];
let x be set;
assume x in the carrier of sum_of(R,S);
assume not thesis;
then [x,x] in IR \/ IS \/ RS \/ SR by NECKLA_2:def 3;
then [x,x] in IR \/ IS \/ RS or [x,x] in SR by XBOOLE_0:def 3;
then
A2: [x,x] in IR \/ IS or [x,x] in RS or [x,x] in SR by XBOOLE_0:def 3;
per cases by A2,XBOOLE_0:def 3;
suppose
A3: [x,x] in IR;
then x in the carrier of R by ZFMISC_1:87;
hence thesis by A3,NECKLACE:def 5;
end;
suppose
A4: [x,x] in IS;
then x in the carrier of S by ZFMISC_1:87;
hence thesis by A4,NECKLACE:def 5;
end;
suppose
[x,x] in RS;
then x in the carrier of R & x in the carrier of S by ZFMISC_1:87;
hence thesis by A1,XBOOLE_0:3;
end;
suppose
[x,x] in SR;
then x in the carrier of S & x in the carrier of R by ZFMISC_1:87;
hence thesis by A1,XBOOLE_0:3;
end;
end;
hence thesis;
end;
theorem Th8:
for R1,R2 being RelStr holds union_of(R1,R2) = union_of(R2,R1) &
sum_of(R1,R2) = sum_of(R2,R1)
proof
let R1,R2 be RelStr;
set U1 = union_of(R1,R2), S1 = sum_of(R1,R2);
A1: the carrier of S1 = (the carrier of R2) \/ the carrier of R1 by
NECKLA_2:def 3;
A2: the InternalRel of S1 = (the InternalRel of R1) \/ (the InternalRel of
R2 ) \/ [:the carrier of R1, the carrier of R2:] \/ [:the carrier of R2, the
carrier of R1:] by NECKLA_2:def 3
.= (the InternalRel of R2) \/ (the InternalRel of R1) \/ [:the carrier
of R2, the carrier of R1:] \/ [:the carrier of R1, the carrier of R2:] by
XBOOLE_1:4;
the carrier of U1 = (the carrier of R2) \/ the carrier of R1 & the
InternalRel of U1 = (the InternalRel of R2) \/ the InternalRel of R1 by
NECKLA_2:def 2;
hence thesis by A1,A2,NECKLA_2:def 2,def 3;
end;
theorem Th9:
for G being irreflexive RelStr, G1,G2 being RelStr st ( G =
union_of(G1,G2) or G = sum_of(G1,G2) ) holds G1 is irreflexive & G2 is
irreflexive
proof
let G be irreflexive RelStr, G1,G2 be RelStr;
assume
A1: G = union_of(G1,G2) or G = sum_of(G1,G2);
per cases by A1;
suppose
A2: G = union_of(G1,G2);
assume
A3: not thesis;
thus thesis
proof
per cases by A3;
suppose
not G1 is irreflexive;
then consider x being set such that
A4: x in the carrier of G1 and
A5: [x,x] in the InternalRel of G1;
[x,x] in (the InternalRel of G1) \/ the InternalRel of G2 by A5,
XBOOLE_0:def 3;
then
A6: [x,x] in the InternalRel of G by A2,NECKLA_2:def 2;
x in (the carrier of G1) \/ the carrier of G2 by A4,XBOOLE_0:def 3;
then x in the carrier of G by A2,NECKLA_2:def 2;
hence thesis by A6,NECKLACE:def 5;
end;
suppose
not G2 is irreflexive;
then consider x being set such that
A7: x in the carrier of G2 and
A8: [x,x] in the InternalRel of G2;
[x,x] in (the InternalRel of G1) \/ the InternalRel of G2 by A8,
XBOOLE_0:def 3;
then
A9: [x,x] in the InternalRel of G by A2,NECKLA_2:def 2;
x in (the carrier of G1) \/ the carrier of G2 by A7,XBOOLE_0:def 3;
then x in the carrier of G by A2,NECKLA_2:def 2;
hence thesis by A9,NECKLACE:def 5;
end;
end;
end;
suppose
A10: G = sum_of(G1,G2);
assume
A11: not thesis;
thus thesis
proof
per cases by A11;
suppose
not G1 is irreflexive;
then consider x being set such that
A12: x in the carrier of G1 and
A13: [x,x] in the InternalRel of G1;
[x,x] in (the InternalRel of G1) \/ the InternalRel of G2 by A13,
XBOOLE_0:def 3;
then
[x,x] in (the InternalRel of G1) \/ (the InternalRel of G2) \/ [:
the carrier of G1,the carrier of G2:] by XBOOLE_0:def 3;
then
[x,x] in (the InternalRel of G1) \/ (the InternalRel of G2) \/ [:
the carrier of G1,the carrier of G2:] \/ [:the carrier of G2,the carrier of G1
:] by XBOOLE_0:def 3;
then
A14: [x,x] in the InternalRel of G by A10,NECKLA_2:def 3;
x in (the carrier of G1) \/ the carrier of G2 by A12,XBOOLE_0:def 3;
then x in the carrier of G by A10,NECKLA_2:def 3;
hence thesis by A14,NECKLACE:def 5;
end;
suppose
not G2 is irreflexive;
then consider x being set such that
A15: x in the carrier of G2 and
A16: [x,x] in the InternalRel of G2;
[x,x] in (the InternalRel of G1) \/ the InternalRel of G2 by A16,
XBOOLE_0:def 3;
then
[x,x] in (the InternalRel of G1) \/ (the InternalRel of G2) \/ [:
the carrier of G1,the carrier of G2:] by XBOOLE_0:def 3;
then
[x,x] in (the InternalRel of G1) \/ (the InternalRel of G2) \/ [:
the carrier of G1,the carrier of G2:] \/ [:the carrier of G2,the carrier of G1
:] by XBOOLE_0:def 3;
then
A17: [x,x] in the InternalRel of G by A10,NECKLA_2:def 3;
x in (the carrier of G1) \/ the carrier of G2 by A15,XBOOLE_0:def 3;
then x in the carrier of G by A10,NECKLA_2:def 3;
hence thesis by A17,NECKLACE:def 5;
end;
end;
end;
end;
theorem Th10:
for G being non empty RelStr, H1,H2 being RelStr st the carrier
of H1 misses the carrier of H2 & ( the RelStr of G = union_of(H1,H2) or the
RelStr of G = sum_of(H1,H2) ) holds H1 is full SubRelStr of G & H2 is full
SubRelStr of G
proof
let G be non empty RelStr;
let H1,H2 be RelStr;
assume that
A1: the carrier of H1 misses the carrier of H2 and
A2: the RelStr of G = union_of(H1,H2) or the RelStr of G = sum_of(H1,H2);
set cH1 = the carrier of H1, cH2 = the carrier of H2, IH1 = the InternalRel
of H1, IH2 = the InternalRel of H2, H1H2 = [:cH1,cH2:], H2H1 = [:cH2,cH1:];
per cases by A2;
suppose
A3: the RelStr of G = union_of(H1,H2);
A4: IH2 = (the InternalRel of G)|_2 cH2
proof
thus IH2 c= (the InternalRel of G)|_2 cH2
proof
let a be object;
the InternalRel of G = IH1 \/ IH2 by A3,NECKLA_2:def 2;
then
A5: IH2 c= the InternalRel of G by XBOOLE_1:7;
assume a in IH2;
hence thesis by A5,XBOOLE_0:def 4;
end;
let a be object;
assume
A6: a in (the InternalRel of G)|_2 cH2;
then
A7: a in [:cH2,cH2:] by XBOOLE_0:def 4;
a in the InternalRel of G by A6,XBOOLE_0:def 4;
then
A8: a in IH1 \/ IH2 by A3,NECKLA_2:def 2;
per cases by A8,XBOOLE_0:def 3;
suppose
a in IH1;
then consider x,y being object such that
A9: a = [x,y] and
A10: x in cH1 and
y in cH1 by RELSET_1:2;
consider x1,y1 being object such that
A11: x1 in cH2 and
y1 in cH2 and
A12: a = [x1,y1] by A7,ZFMISC_1:def 2;
x = x1 by A9,A12,XTUPLE_0:1;
then cH1 /\ cH2 <> {} by A10,A11,XBOOLE_0:def 4;
hence thesis by A1;
end;
suppose
a in IH2;
hence thesis;
end;
end;
A13: IH1 = (the InternalRel of G)|_2 cH1
proof
thus IH1 c= (the InternalRel of G)|_2 cH1
proof
let a be object;
the InternalRel of G = IH1 \/ IH2 by A3,NECKLA_2:def 2;
then
A14: IH1 c= the InternalRel of G by XBOOLE_1:7;
assume a in IH1;
hence thesis by A14,XBOOLE_0:def 4;
end;
let a be object;
assume
A15: a in (the InternalRel of G)|_2 cH1;
then
A16: a in [:cH1,cH1:] by XBOOLE_0:def 4;
a in the InternalRel of G by A15,XBOOLE_0:def 4;
then
A17: a in IH1 \/ IH2 by A3,NECKLA_2:def 2;
per cases by A17,XBOOLE_0:def 3;
suppose
a in IH1;
hence thesis;
end;
suppose
a in IH2;
then consider x,y being object such that
A18: a = [x,y] and
A19: x in cH2 and
y in cH2 by RELSET_1:2;
ex x1,y1 being object st x1 in cH1 & y1 in cH1 & a = [x1,y1 ] by A16,
ZFMISC_1:def 2;
then x in cH1 by A18,XTUPLE_0:1;
hence thesis by A1,A19,XBOOLE_0:3;
end;
end;
the carrier of G = (the carrier of H1) \/ (the carrier of H2) by A3,
NECKLA_2:def 2;
then
A20: the carrier of H1 c= the carrier of G & the carrier of H2 c= the
carrier of G by XBOOLE_1:7;
the InternalRel of G = IH1 \/ IH2 by A3,NECKLA_2:def 2;
then
IH1 c= the InternalRel of G & the InternalRel of H2 c= the InternalRel
of G by XBOOLE_1:7;
hence thesis by A20,A13,A4,YELLOW_0:def 13,def 14;
end;
suppose
A21: the RelStr of G = sum_of(H1,H2);
A22: IH2 = (the InternalRel of G)|_2 cH2
proof
thus IH2 c= (the InternalRel of G)|_2 cH2
proof
let a be object;
the InternalRel of G = IH1 \/ IH2 \/ H1H2 \/ H2H1 by A21,NECKLA_2:def 3
;
then the InternalRel of G = IH2 \/ (IH1 \/ H1H2 \/ H2H1) by
XBOOLE_1:113;
then
A23: IH2 c= the InternalRel of G by XBOOLE_1:7;
assume a in IH2;
hence thesis by A23,XBOOLE_0:def 4;
end;
let a be object;
assume
A24: a in (the InternalRel of G)|_2 cH2;
then
A25: a in [:cH2,cH2:] by XBOOLE_0:def 4;
a in the InternalRel of G by A24,XBOOLE_0:def 4;
then a in IH1 \/ IH2 \/ H1H2 \/ H2H1 by A21,NECKLA_2:def 3;
then a in IH1 \/ (IH2 \/ H1H2 \/ H2H1) by XBOOLE_1:113;
then a in IH1 or a in IH2 \/ H1H2 \/ H2H1 by XBOOLE_0:def 3;
then a in IH1 or a in IH2 \/ (H1H2 \/ H2H1) by XBOOLE_1:4;
then
A26: a in IH1 or a in IH2 or a in H1H2 \/ H2H1 by XBOOLE_0:def 3;
per cases by A26,XBOOLE_0:def 3;
suppose
a in IH1;
then consider x,y being object such that
A27: a = [x,y] and
A28: x in cH1 and
y in cH1 by RELSET_1:2;
consider x1,y1 being object such that
A29: x1 in cH2 and
y1 in cH2 and
A30: a = [x1,y1] by A25,ZFMISC_1:def 2;
x = x1 by A27,A30,XTUPLE_0:1;
then cH1 /\ cH2 <> {} by A28,A29,XBOOLE_0:def 4;
hence thesis by A1;
end;
suppose
a in IH2;
hence thesis;
end;
suppose
a in H1H2;
then consider x,y being object such that
A31: x in cH1 and
y in cH2 and
A32: a = [x,y] by ZFMISC_1:def 2;
consider x1,y1 being object such that
A33: x1 in cH2 and
y1 in cH2 and
A34: a = [x1,y1] by A25,ZFMISC_1:def 2;
x = x1 by A32,A34,XTUPLE_0:1;
then cH1 /\ cH2 <> {} by A31,A33,XBOOLE_0:def 4;
hence thesis by A1;
end;
suppose
a in H2H1;
then consider x,y being object such that
x in cH2 and
A35: y in cH1 and
A36: a = [x,y] by ZFMISC_1:def 2;
consider x1,y1 being object such that
x1 in cH2 and
A37: y1 in cH2 and
A38: a = [x1,y1] by A25,ZFMISC_1:def 2;
y = y1 by A36,A38,XTUPLE_0:1;
then cH1 /\ cH2 <> {} by A35,A37,XBOOLE_0:def 4;
hence thesis by A1;
end;
end;
IH2 c= IH1 \/ IH2 \/ [:cH1, cH2:] by XBOOLE_1:7,10;
then
A39: IH2 c= IH1 \/ IH2 \/ [:cH1, cH2:] \/ [:cH2, cH1:] by XBOOLE_1:10;
A40: IH1 = (the InternalRel of G)|_2 cH1
proof
thus IH1 c= (the InternalRel of G)|_2 cH1
proof
let a be object;
the InternalRel of G = IH1 \/ IH2 \/ H1H2 \/ H2H1 by A21,NECKLA_2:def 3
.= IH1 \/ (IH2 \/ H1H2 \/ H2H1) by XBOOLE_1:113;
then
A41: IH1 c= the InternalRel of G by XBOOLE_1:7;
assume a in IH1;
hence thesis by A41,XBOOLE_0:def 4;
end;
let a be object;
assume
A42: a in (the InternalRel of G)|_2 cH1;
then
A43: a in [:cH1,cH1:] by XBOOLE_0:def 4;
a in the InternalRel of G by A42,XBOOLE_0:def 4;
then a in IH1 \/ IH2 \/ H1H2 \/ H2H1 by A21,NECKLA_2:def 3;
then a in IH1 \/ (IH2 \/ H1H2 \/ H2H1) by XBOOLE_1:113;
then a in IH1 or a in IH2 \/ H1H2 \/ H2H1 by XBOOLE_0:def 3;
then a in IH1 or a in IH2 \/ (H1H2 \/ H2H1) by XBOOLE_1:4;
then
A44: a in IH1 or a in IH2 or a in H1H2 \/ H2H1 by XBOOLE_0:def 3;
per cases by A44,XBOOLE_0:def 3;
suppose
a in IH1;
hence thesis;
end;
suppose
a in IH2;
then consider x,y being object such that
A45: a = [x,y] and
A46: x in cH2 and
y in cH2 by RELSET_1:2;
consider x1,y1 being object such that
A47: x1 in cH1 and
y1 in cH1 and
A48: a = [x1,y1] by A43,ZFMISC_1:def 2;
x = x1 by A45,A48,XTUPLE_0:1;
then cH1 /\ cH2 <> {} by A46,A47,XBOOLE_0:def 4;
hence thesis by A1;
end;
suppose
a in H1H2;
then consider x,y being object such that
x in cH1 and
A49: y in cH2 and
A50: a = [x,y] by ZFMISC_1:def 2;
consider x1,y1 being object such that
x1 in cH1 and
A51: y1 in cH1 and
A52: a = [x1,y1] by A43,ZFMISC_1:def 2;
y = y1 by A50,A52,XTUPLE_0:1;
then cH1 /\ cH2 <> {} by A49,A51,XBOOLE_0:def 4;
hence thesis by A1;
end;
suppose
a in H2H1;
then consider x,y being object such that
A53: x in cH2 and
y in cH1 and
A54: a = [x,y] by ZFMISC_1:def 2;
consider x1,y1 being object such that
A55: x1 in cH1 and
y1 in cH1 and
A56: a = [x1,y1] by A43,ZFMISC_1:def 2;
x = x1 by A54,A56,XTUPLE_0:1;
then cH1 /\ cH2 <> {} by A53,A55,XBOOLE_0:def 4;
hence thesis by A1;
end;
end;
IH1 c= IH1 \/ (IH2 \/ [:cH1, cH2:]) by XBOOLE_1:7;
then
A57: IH1 c= IH1 \/ IH2 \/ [:cH1, cH2:] by XBOOLE_1:4;
the carrier of G = (the carrier of H1) \/ (the carrier of H2) by A21,
NECKLA_2:def 3;
then
A58: the carrier of H1 c= the carrier of G & the carrier of H2 c= the
carrier of G by XBOOLE_1:7;
A59: the InternalRel of G = IH1 \/ IH2 \/ [:cH1, cH2:] \/ [:cH2, cH1:] by A21,
NECKLA_2:def 3;
then IH1 \/ IH2 \/ [:cH1, cH2:] c= the InternalRel of G by XBOOLE_1:7;
then IH1 c= the InternalRel of G by A57;
hence thesis by A59,A58,A39,A40,A22,YELLOW_0:def 13,def 14;
end;
end;
begin :: Theorems relating to the complement of RelStr
theorem Th11:
the InternalRel of ComplRelStr Necklace 4 = {[0,2],[2,0],[0,3],[
3,0],[1,3],[3,1]}
proof
set N4 = Necklace 4, cN4 = the carrier of N4, CmpN4 = ComplRelStr N4;
A1: the carrier of Necklace 4 = {0,1,2,3} by NECKLACE:1,20;
thus the InternalRel of CmpN4 c= {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]}
proof
let x be object;
assume x in the InternalRel of CmpN4;
then
A2: x in (the InternalRel of N4)` \ id cN4 by NECKLACE:def 8;
then
A3: not x in id cN4 by XBOOLE_0:def 5;
x in (the InternalRel of N4)` by A2,XBOOLE_0:def 5;
then
A4: x in [:cN4,cN4:] \ (the InternalRel of N4) by SUBSET_1:def 4;
consider a1,b1 being object such that
A5: a1 in cN4 and
A6: b1 in cN4 and
A7: x = [a1,b1] by A2,ZFMISC_1:def 2;
per cases by A1,A5,A6,ENUMSET1:def 2;
suppose
a1 = 0 & b1 = 0;
hence thesis by A3,A5,A7,RELAT_1:def 10;
end;
suppose
a1 = 0 & b1 = 1;
then x in the InternalRel of N4 by A7,ENUMSET1:def 4,NECKLA_2:2;
hence thesis by A4,XBOOLE_0:def 5;
end;
suppose
a1 = 0 & b1 = 2;
hence thesis by A7,ENUMSET1:def 4;
end;
suppose
a1 = 0 & b1 = 3;
hence thesis by A7,ENUMSET1:def 4;
end;
suppose
a1 = 1 & b1 = 0;
then x in the InternalRel of N4 by A7,ENUMSET1:def 4,NECKLA_2:2;
hence thesis by A4,XBOOLE_0:def 5;
end;
suppose
a1 = 2 & b1 = 0;
hence thesis by A7,ENUMSET1:def 4;
end;
suppose
a1 = 3 & b1 = 0;
hence thesis by A7,ENUMSET1:def 4;
end;
suppose
a1 = 1 & b1 = 1;
hence thesis by A3,A5,A7,RELAT_1:def 10;
end;
suppose
a1 = 1 & b1 = 2;
then x in the InternalRel of N4 by A7,ENUMSET1:def 4,NECKLA_2:2;
hence thesis by A4,XBOOLE_0:def 5;
end;
suppose
a1 = 1 & b1 = 3;
hence thesis by A7,ENUMSET1:def 4;
end;
suppose
a1 = 2 & b1 = 2;
hence thesis by A3,A5,A7,RELAT_1:def 10;
end;
suppose
a1 = 2 & b1 = 1;
then x in the InternalRel of N4 by A7,ENUMSET1:def 4,NECKLA_2:2;
hence thesis by A4,XBOOLE_0:def 5;
end;
suppose
a1 = 2 & b1 = 3;
then x in the InternalRel of N4 by A7,ENUMSET1:def 4,NECKLA_2:2;
hence thesis by A4,XBOOLE_0:def 5;
end;
suppose
a1 = 3 & b1 = 3;
hence thesis by A3,A5,A7,RELAT_1:def 10;
end;
suppose
a1 = 3 & b1 = 1;
hence thesis by A7,ENUMSET1:def 4;
end;
suppose
a1 = 3 & b1 = 2;
then x in the InternalRel of N4 by A7,ENUMSET1:def 4,NECKLA_2:2;
hence thesis by A4,XBOOLE_0:def 5;
end;
end;
let a be object;
assume
A8: a in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]};
per cases by A8,ENUMSET1:def 4;
suppose
A9: a = [0,2];
A10: not a in the InternalRel of N4
proof
assume
A11: not thesis;
per cases by A11,ENUMSET1:def 4,NECKLA_2:2;
suppose
a = [0,1];
hence contradiction by A9,XTUPLE_0:1;
end;
suppose
a = [1,0];
hence contradiction by A9,XTUPLE_0:1;
end;
suppose
a = [1,2];
hence contradiction by A9,XTUPLE_0:1;
end;
suppose
a = [2,1];
hence contradiction by A9,XTUPLE_0:1;
end;
suppose
a = [2,3];
hence contradiction by A9,XTUPLE_0:1;
end;
suppose
a = [3,2];
hence contradiction by A9,XTUPLE_0:1;
end;
end;
0 in cN4 & 2 in cN4 by A1,ENUMSET1:def 2;
then a in [:cN4,cN4:] by A9,ZFMISC_1:87;
then a in [:cN4,cN4:]\ (the InternalRel of N4) by A10,XBOOLE_0:def 5;
then
A12: a in (the InternalRel of N4)` by SUBSET_1:def 4;
not a in id cN4 by A9,RELAT_1:def 10;
then a in (the InternalRel of N4)` \ id cN4 by A12,XBOOLE_0:def 5;
hence thesis by NECKLACE:def 8;
end;
suppose
A13: a = [2,0];
A14: not a in the InternalRel of N4
proof
assume
A15: not thesis;
per cases by A15,ENUMSET1:def 4,NECKLA_2:2;
suppose
a = [0,1];
hence contradiction by A13,XTUPLE_0:1;
end;
suppose
a = [1,0];
hence contradiction by A13,XTUPLE_0:1;
end;
suppose
a = [1,2];
hence contradiction by A13,XTUPLE_0:1;
end;
suppose
a = [2,1];
hence contradiction by A13,XTUPLE_0:1;
end;
suppose
a = [2,3];
hence contradiction by A13,XTUPLE_0:1;
end;
suppose
a = [3,2];
hence contradiction by A13,XTUPLE_0:1;
end;
end;
0 in cN4 & 2 in cN4 by A1,ENUMSET1:def 2;
then a in [:cN4,cN4:] by A13,ZFMISC_1:87;
then a in [:cN4,cN4:]\ (the InternalRel of N4) by A14,XBOOLE_0:def 5;
then
A16: a in (the InternalRel of N4)` by SUBSET_1:def 4;
not a in id cN4 by A13,RELAT_1:def 10;
then a in (the InternalRel of N4)` \ id cN4 by A16,XBOOLE_0:def 5;
hence thesis by NECKLACE:def 8;
end;
suppose
A17: a = [0,3];
A18: not a in the InternalRel of N4
proof
assume
A19: not thesis;
per cases by A19,ENUMSET1:def 4,NECKLA_2:2;
suppose
a = [0,1];
hence contradiction by A17,XTUPLE_0:1;
end;
suppose
a = [1,0];
hence contradiction by A17,XTUPLE_0:1;
end;
suppose
a = [1,2];
hence contradiction by A17,XTUPLE_0:1;
end;
suppose
a = [2,1];
hence contradiction by A17,XTUPLE_0:1;
end;
suppose
a = [2,3];
hence contradiction by A17,XTUPLE_0:1;
end;
suppose
a = [3,2];
hence contradiction by A17,XTUPLE_0:1;
end;
end;
0 in cN4 & 3 in cN4 by A1,ENUMSET1:def 2;
then a in [:cN4,cN4:] by A17,ZFMISC_1:87;
then a in [:cN4,cN4:]\ (the InternalRel of N4) by A18,XBOOLE_0:def 5;
then
A20: a in (the InternalRel of N4)` by SUBSET_1:def 4;
not a in id cN4 by A17,RELAT_1:def 10;
then a in (the InternalRel of N4)` \ id cN4 by A20,XBOOLE_0:def 5;
hence thesis by NECKLACE:def 8;
end;
suppose
A21: a = [3,0];
A22: not a in the InternalRel of N4
proof
assume
A23: not thesis;
per cases by A23,ENUMSET1:def 4,NECKLA_2:2;
suppose
a = [0,1];
hence contradiction by A21,XTUPLE_0:1;
end;
suppose
a = [1,0];
hence contradiction by A21,XTUPLE_0:1;
end;
suppose
a = [1,2];
hence contradiction by A21,XTUPLE_0:1;
end;
suppose
a = [2,1];
hence contradiction by A21,XTUPLE_0:1;
end;
suppose
a = [2,3];
hence contradiction by A21,XTUPLE_0:1;
end;
suppose
a = [3,2];
hence contradiction by A21,XTUPLE_0:1;
end;
end;
0 in cN4 & 3 in cN4 by A1,ENUMSET1:def 2;
then a in [:cN4,cN4:] by A21,ZFMISC_1:87;
then a in [:cN4,cN4:]\ (the InternalRel of N4) by A22,XBOOLE_0:def 5;
then
A24: a in (the InternalRel of N4)` by SUBSET_1:def 4;
not a in id cN4 by A21,RELAT_1:def 10;
then a in (the InternalRel of N4)` \ id cN4 by A24,XBOOLE_0:def 5;
hence thesis by NECKLACE:def 8;
end;
suppose
A25: a = [1,3];
A26: not a in the InternalRel of N4
proof
assume
A27: not thesis;
per cases by A27,ENUMSET1:def 4,NECKLA_2:2;
suppose
a = [0,1];
hence contradiction by A25,XTUPLE_0:1;
end;
suppose
a = [1,0];
hence contradiction by A25,XTUPLE_0:1;
end;
suppose
a = [1,2];
hence contradiction by A25,XTUPLE_0:1;
end;
suppose
a = [2,1];
hence contradiction by A25,XTUPLE_0:1;
end;
suppose
a = [2,3];
hence contradiction by A25,XTUPLE_0:1;
end;
suppose
a = [3,2];
hence contradiction by A25,XTUPLE_0:1;
end;
end;
1 in cN4 & 3 in cN4 by A1,ENUMSET1:def 2;
then a in [:cN4,cN4:] by A25,ZFMISC_1:87;
then a in [:cN4,cN4:]\ (the InternalRel of N4) by A26,XBOOLE_0:def 5;
then
A28: a in (the InternalRel of N4)` by SUBSET_1:def 4;
not a in id cN4 by A25,RELAT_1:def 10;
then a in (the InternalRel of N4)` \ id cN4 by A28,XBOOLE_0:def 5;
hence thesis by NECKLACE:def 8;
end;
suppose
A29: a = [3,1];
A30: not a in the InternalRel of N4
proof
assume
A31: not thesis;
per cases by A31,ENUMSET1:def 4,NECKLA_2:2;
suppose
a = [0,1];
hence contradiction by A29,XTUPLE_0:1;
end;
suppose
a = [1,0];
hence contradiction by A29,XTUPLE_0:1;
end;
suppose
a = [1,2];
hence contradiction by A29,XTUPLE_0:1;
end;
suppose
a = [2,1];
hence contradiction by A29,XTUPLE_0:1;
end;
suppose
a = [2,3];
hence contradiction by A29,XTUPLE_0:1;
end;
suppose
a = [3,2];
hence contradiction by A29,XTUPLE_0:1;
end;
end;
1 in cN4 & 3 in cN4 by A1,ENUMSET1:def 2;
then a in [:cN4,cN4:] by A29,ZFMISC_1:87;
then a in [:cN4,cN4:]\ (the InternalRel of N4) by A30,XBOOLE_0:def 5;
then
A32: a in (the InternalRel of N4)` by SUBSET_1:def 4;
not a in id cN4 by A29,RELAT_1:def 10;
then a in (the InternalRel of N4)` \ id cN4 by A32,XBOOLE_0:def 5;
hence thesis by NECKLACE:def 8;
end;
end;
registration
let R be RelStr;
cluster ComplRelStr R -> irreflexive;
correctness
proof
set R1 = ComplRelStr R;
for x being set st x in the carrier of R1 holds not [x,x] in the
InternalRel of R1
proof
let x be set;
assume x in the carrier of R1;
then
A1: x in the carrier of R by NECKLACE:def 8;
not [x,x] in the InternalRel of R1
proof
assume [x,x] in the InternalRel of R1;
then [x,x] in (the InternalRel of R)` \ id (the carrier of R) by
NECKLACE:def 8;
then not [x,x] in id (the carrier of R) by XBOOLE_0:def 5;
hence contradiction by A1,RELAT_1:def 10;
end;
hence thesis;
end;
hence thesis;
end;
end;
registration
let R be symmetric RelStr;
cluster ComplRelStr R -> symmetric;
correctness
proof
let x,y be object;
set S = ComplRelStr R;
assume that
A1: x in the carrier of S & y in the carrier of S and
A2: [x,y] in the InternalRel of S;
per cases;
suppose
x = y;
hence thesis by A2;
end;
suppose
A3: x <> y;
A4: x in the carrier of R & y in the carrier of R by A1,NECKLACE:def 8;
then
A5: [y,x] in [:the carrier of R,the carrier of R:] by ZFMISC_1:87;
[x,y] in (the InternalRel of R)` \ id (the carrier of R) by A2,
NECKLACE:def 8;
then [x,y] in (the InternalRel of R)` by XBOOLE_0:def 5;
then
[x,y] in [:the carrier of R,the carrier of R:] \ (the InternalRel of
R) by SUBSET_1:def 4;
then
A6: not [x,y] in the InternalRel of R by XBOOLE_0:def 5;
the InternalRel of R is_symmetric_in the carrier of R by NECKLACE:def 3;
then not [y,x] in the InternalRel of R by A4,A6;
then [y,x] in [:the carrier of R,the carrier of R:] \ (the InternalRel
of R) by A5,XBOOLE_0:def 5;
then
A7: [y,x] in (the InternalRel of R)` by SUBSET_1:def 4;
not [y,x] in id (the carrier of R) by A3,RELAT_1:def 10;
then [y,x] in (the InternalRel of R)` \ id (the carrier of R) by A7,
XBOOLE_0:def 5;
hence thesis by NECKLACE:def 8;
end;
end;
end;
theorem Th12:
for R be RelStr holds the InternalRel of R misses the
InternalRel of ComplRelStr R
proof
let R be RelStr;
assume not thesis;
then (the InternalRel of R) /\ the InternalRel of ComplRelStr R <> {};
then consider a being object such that
A1: a in (the InternalRel of R) /\ the InternalRel of ComplRelStr R by
XBOOLE_0:def 1;
a in the InternalRel of ComplRelStr R by A1,XBOOLE_0:def 4;
then a in (the InternalRel of R)` \ id (the carrier of R) by NECKLACE:def 8;
then a in (the InternalRel of R)` by XBOOLE_0:def 5;
then a in [:the carrier of R,the carrier of R:] \ (the InternalRel of R) by
SUBSET_1:def 4;
then not a in the InternalRel of R by XBOOLE_0:def 5;
hence thesis by A1,XBOOLE_0:def 4;
end;
theorem Th13:
for R being RelStr holds id the carrier of R misses the
InternalRel of ComplRelStr R
proof
let R be RelStr;
assume not thesis;
then id (the carrier of R) /\ the InternalRel of ComplRelStr R <> {};
then consider a being object such that
A1: a in id (the carrier of R) /\ the InternalRel of ComplRelStr R by
XBOOLE_0:def 1;
a in the InternalRel of ComplRelStr R by A1,XBOOLE_0:def 4;
then
A2: a in (the InternalRel of R)` \ id the carrier of R by NECKLACE:def 8;
a in id (the carrier of R) by A1,XBOOLE_0:def 4;
hence contradiction by A2,XBOOLE_0:def 5;
end;
theorem Th14:
for G being RelStr holds [:the carrier of G,the carrier of G:] =
id (the carrier of G) \/ (the InternalRel of G) \/ (the InternalRel of
ComplRelStr G)
proof
let G be RelStr;
set idcG = id the carrier of G, IG = the InternalRel of G, ICmpG = the
InternalRel of ComplRelStr G, cG = the carrier of G;
thus [:cG,cG:] c= idcG \/ IG \/ ICmpG
proof
let a be object;
assume
A1: a in [:cG,cG:];
then consider x,y being object such that
A2: x in cG and
y in cG and
A3: a = [x,y] by ZFMISC_1:def 2;
per cases;
suppose
A4: x = y;
[x,x] in id cG by A2,RELAT_1:def 10;
then a in id cG \/ IG by A3,A4,XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 3;
end;
suppose
x <> y;
then
A5: not a in id cG by A3,RELAT_1:def 10;
thus thesis
proof
per cases;
suppose
a in IG;
then a in id cG \/ IG by XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 3;
end;
suppose
not a in IG;
then a in [:cG,cG:] \ IG by A1,XBOOLE_0:def 5;
then a in IG` by SUBSET_1:def 4;
then a in IG` \ id cG by A5,XBOOLE_0:def 5;
then a in ICmpG by NECKLACE:def 8;
then a in IG \/ ICmpG by XBOOLE_0:def 3;
then a in id cG \/ (IG \/ ICmpG) by XBOOLE_0:def 3;
hence thesis by XBOOLE_1:4;
end;
end;
end;
end;
let a be object;
assume a in idcG \/ IG \/ ICmpG;
then
A6: a in id cG \/ IG or a in ICmpG by XBOOLE_0:def 3;
per cases by A6,XBOOLE_0:def 3;
suppose
a in id cG;
hence thesis;
end;
suppose
a in IG;
hence thesis;
end;
suppose
a in ICmpG;
then a in IG` \ id cG by NECKLACE:def 8;
hence thesis;
end;
end;
theorem Th15:
for G being strict irreflexive RelStr st G is trivial holds ComplRelStr G = G
proof
let G be strict irreflexive RelStr;
set CG = ComplRelStr G;
assume
A1: G is trivial;
per cases by A1,ZFMISC_1:131;
suppose
A2: the carrier of G is empty;
the InternalRel of CG = (the InternalRel of G)` \ id (the carrier of G
) by NECKLACE:def 8;
then
A3: the InternalRel of CG = ({} \ {}) \ id {} by A2;
the InternalRel of G = {} by A2;
hence thesis by A3,NECKLACE:def 8;
end;
suppose
ex x being object st the carrier of G = {x};
then consider x being object such that
A4: the carrier of G = {x};
A5: the carrier of CG = {x} by A4,NECKLACE:def 8;
the InternalRel of G c= [:{x},{x}:] by A4;
then the InternalRel of G c= {[x,x]} by ZFMISC_1:29;
then
A6: the InternalRel of G = {} or the InternalRel of G = {[x,x]} by ZFMISC_1:33;
A7: the InternalRel of G <> {[x,x]}
proof
assume not thesis;
then
A8: [x,x] in the InternalRel of G by TARSKI:def 1;
x in the carrier of G by A4,TARSKI:def 1;
hence contradiction by A8,NECKLACE:def 5;
end;
the InternalRel of CG = (the InternalRel of G)` \ id (the carrier of
G) by NECKLACE:def 8;
then the InternalRel of CG = ([:{x},{x}:] \ {}) \ id {x} by A4,A6,A7,
SUBSET_1:def 4;
then the InternalRel of CG = {[x,x]} \ id {x} by ZFMISC_1:29;
then the InternalRel of CG = {[x,x]} \ {[x,x]} by SYSREL:13;
hence thesis by A4,A6,A7,A5,XBOOLE_1:37;
end;
end;
theorem Th16:
for G being strict irreflexive RelStr holds ComplRelStr ( ComplRelStr G) = G
proof
let G be strict irreflexive RelStr;
set CCmpG = ComplRelStr (ComplRelStr G), CmpG = ComplRelStr G, cG = the
carrier of G, IG = the InternalRel of G, ICmpG = the InternalRel of CmpG,
ICCmpG = the InternalRel of CCmpG;
A1: cG = the carrier of CmpG by NECKLACE:def 8
.= the carrier of CCmpG by NECKLACE:def 8;
A2: cG = the carrier of CmpG by NECKLACE:def 8;
A3: id cG misses IG
proof
assume not thesis;
then id cG /\ IG <> {};
then consider a being object such that
A4: a in id cG /\ IG by XBOOLE_0:def 1;
A5: a in IG by A4,XBOOLE_0:def 4;
consider x,y being object such that
A6: a = [x,y] and
A7: x in cG and
y in cG by A4,RELSET_1:2;
a in id cG by A4,XBOOLE_0:def 4;
then x = y by A6,RELAT_1:def 10;
hence contradiction by A5,A6,A7,NECKLACE:def 5;
end;
ICCmpG = (ICmpG)` \ id the carrier of CmpG by NECKLACE:def 8
.= [:the carrier of CmpG,the carrier of CmpG:] \ ICmpG \ id the carrier
of CmpG by SUBSET_1:def 4
.= ([:cG,cG:] \ (IG` \ id cG)) \ id cG by A2,NECKLACE:def 8
.= (([:cG,cG:] \ IG`) \/ ([:cG,cG:] /\ id cG)) \ id cG by XBOOLE_1:52
.= ( ([:cG,cG:] \ IG`) \/ id cG ) \ id cG by XBOOLE_1:28
.= ([:cG,cG:] \ IG`) \ id cG by XBOOLE_1:40
.= ([:cG,cG:] \ ([:cG,cG:] \ IG)) \ id cG by SUBSET_1:def 4
.= ([:cG,cG:] /\ IG) \ id cG by XBOOLE_1:48
.= IG \ id cG by XBOOLE_1:28
.= IG by A3,XBOOLE_1:83;
hence thesis by A1;
end;
theorem Th17:
for G1,G2 being RelStr st the carrier of G1 misses the carrier
of G2 holds ComplRelStr union_of(G1,G2) = sum_of(ComplRelStr G1, ComplRelStr G2
)
proof
let G1,G2 be RelStr;
A1: the carrier of sum_of(ComplRelStr G1, ComplRelStr G2) = (the carrier of
ComplRelStr G1) \/ (the carrier of ComplRelStr G2) by NECKLA_2:def 3
.= (the carrier of G1) \/ the carrier of ComplRelStr G2 by NECKLACE:def 8
.= (the carrier of G1) \/ the carrier of G2 by NECKLACE:def 8;
set P = the InternalRel of ComplRelStr union_of(G1,G2), R = the InternalRel
of sum_of(ComplRelStr G1,ComplRelStr G2), X1 = the InternalRel of ComplRelStr
G1, X2 = the InternalRel of ComplRelStr G2, X3 = [:the carrier of ComplRelStr
G1,the carrier of ComplRelStr G2:], X4 = [:the carrier of ComplRelStr G2,the
carrier of ComplRelStr G1:], X5 = [:the carrier of G1, the carrier of G1:], X6
= [:the carrier of G2, the carrier of G2:], X7 = [:the carrier of G1, the
carrier of G2:], X8 = [:the carrier of G2, the carrier of G1:];
assume
A2: the carrier of G1 misses the carrier of G2;
A3: for a,b being object holds [a,b] in P iff [a,b] in R
proof
let a,b be object;
set x = [a,b];
thus x in P implies x in R
proof
assume x in P;
then
A4: x in (the InternalRel of union_of(G1,G2))` \ id the carrier of
union_of(G1,G2) by NECKLACE:def 8;
then x in [:the carrier of union_of(G1,G2),the carrier of union_of( G1,
G2) :];
then x in [:(the carrier of G1) \/ the carrier of G2, the carrier of
union_of(G1,G2):] by NECKLA_2:def 2;
then
A5: x in [:(the carrier of G1) \/ the carrier of G2, (the carrier of G1
) \/ the carrier of G2:] by NECKLA_2:def 2;
not x in id the carrier of union_of(G1,G2) by A4,XBOOLE_0:def 5;
then
A6: not x in id ((the carrier of G1) \/ the carrier of G2) by NECKLA_2:def 2;
A7: not x in id the carrier of G1 & not x in id the carrier of G2
proof
assume not thesis;
then x in id (the carrier of G1) \/ id (the carrier of G2) by
XBOOLE_0:def 3;
hence contradiction by A6,SYSREL:14;
end;
the carrier of G1 = the carrier of ComplRelStr G1 & the carrier of
G2 = the carrier of ComplRelStr G2 by NECKLACE:def 8;
then x in X5 \/ X3 \/ X4 \/ X6 by A5,ZFMISC_1:98;
then x in X5 \/ (X3 \/ X4 \/ X6) by XBOOLE_1:113;
then x in X5 or x in (X3 \/ X4 \/ X6) by XBOOLE_0:def 3;
then x in X5 or x in X3 \/ (X4 \/ X6) by XBOOLE_1:4;
then
A8: x in X5 or x in X3 or x in X4 \/ X6 by XBOOLE_0:def 3;
x in (the InternalRel of union_of(G1,G2))` by A4,XBOOLE_0:def 5;
then
x in [:the carrier of union_of(G1,G2),the carrier of union_of(G1, G2
):] \ (the InternalRel of union_of(G1,G2)) by SUBSET_1:def 4;
then not x in (the InternalRel of union_of(G1,G2)) by XBOOLE_0:def 5;
then
A9: not x in (the InternalRel of G1) \/ the InternalRel of G2 by
NECKLA_2:def 2;
then
A10: not x in the InternalRel of G1 by XBOOLE_0:def 3;
A11: not x in the InternalRel of G2 by A9,XBOOLE_0:def 3;
per cases by A8,XBOOLE_0:def 3;
suppose
x in [:the carrier of G1,the carrier of G1:];
then
x in [:the carrier of G1,the carrier of G1:] \ the InternalRel of
G1 by A10,XBOOLE_0:def 5;
then x in (the InternalRel of G1)` by SUBSET_1:def 4;
then x in (the InternalRel of G1)` \ id the carrier of G1 by A7,
XBOOLE_0:def 5;
then x in X1 by NECKLACE:def 8;
then x in X1 \/ (X2 \/ X3 \/ X4) by XBOOLE_0:def 3;
then x in X1 \/ X2 \/ X3 \/ X4 by XBOOLE_1:113;
hence thesis by NECKLA_2:def 3;
end;
suppose
x in X3;
then x in X2 \/ X3 by XBOOLE_0:def 3;
then x in X2 \/ X3 \/ X4 by XBOOLE_0:def 3;
then x in X1 \/ (X2 \/ X3 \/ X4) by XBOOLE_0:def 3;
then x in X1 \/ X2 \/ X3 \/ X4 by XBOOLE_1:113;
hence thesis by NECKLA_2:def 3;
end;
suppose
x in X4;
then x in X3 \/ X4 by XBOOLE_0:def 3;
then x in X2 \/ (X3 \/ X4) by XBOOLE_0:def 3;
then x in X2 \/ X3 \/ X4 by XBOOLE_1:4;
then x in X1 \/ (X2 \/ X3 \/ X4) by XBOOLE_0:def 3;
then x in X1 \/ X2 \/ X3 \/ X4 by XBOOLE_1:113;
hence thesis by NECKLA_2:def 3;
end;
suppose
x in [:the carrier of G2,the carrier of G2:];
then
x in [:the carrier of G2,the carrier of G2:] \ the InternalRel of
G2 by A11,XBOOLE_0:def 5;
then x in (the InternalRel of G2)` by SUBSET_1:def 4;
then x in (the InternalRel of G2)` \ id the carrier of G2 by A7,
XBOOLE_0:def 5;
then x in the InternalRel of ComplRelStr G2 by NECKLACE:def 8;
then x in (the InternalRel of ComplRelStr G1) \/ (the InternalRel of
ComplRelStr G2) by XBOOLE_0:def 3;
then x in (the InternalRel of ComplRelStr G1) \/ (the InternalRel of
ComplRelStr G2) \/ [:the carrier of ComplRelStr G1, the carrier of ComplRelStr
G2:] by XBOOLE_0:def 3;
then x in (the InternalRel of ComplRelStr G1) \/ (the InternalRel of
ComplRelStr G2) \/ [:the carrier of ComplRelStr G1, the carrier of ComplRelStr
G2:] \/ [:the carrier of ComplRelStr G2, the carrier of ComplRelStr G1:] by
XBOOLE_0:def 3;
hence thesis by NECKLA_2:def 3;
end;
end;
assume x in R;
then x in X1 \/ X2 \/ X3 \/ X4 by NECKLA_2:def 3;
then x in X1 \/ X2 \/ X3 or x in X4 by XBOOLE_0:def 3;
then
A12: x in X1 \/ X2 or x in X3 or x in X4 by XBOOLE_0:def 3;
per cases by A12,XBOOLE_0:def 3;
suppose
x in X1;
then
A13: x in (the InternalRel of G1)` \ id the carrier of G1 by NECKLACE:def 8;
then x in (the InternalRel of G1)` by XBOOLE_0:def 5;
then x in [:the carrier of G1,the carrier of G1:] \ the InternalRel of
G1 by SUBSET_1:def 4;
then
A14: not x in the InternalRel of G1 by XBOOLE_0:def 5;
A15: not x in the InternalRel of union_of(G1,G2)
proof
assume not thesis;
then x in (the InternalRel of G1) \/ the InternalRel of G2 by
NECKLA_2:def 2;
then x in the InternalRel of G2 by A14,XBOOLE_0:def 3;
then [:the carrier of G1,the carrier of G1:] /\ [:the carrier of G2,
the carrier of G2:] is non empty by A13,XBOOLE_0:def 4;
then
[:the carrier of G1,the carrier of G1:] meets [:the carrier of G2
,the carrier of G2:];
hence contradiction by A2,ZFMISC_1:104;
end;
A16: not x in id the carrier of union_of(G1,G2)
proof
assume not thesis;
then x in id ((the carrier of G1) \/ the carrier of G2) by
NECKLA_2:def 2;
then
A17: x in (id the carrier of G1) \/ id the carrier of G2 by SYSREL:14;
thus thesis
proof
per cases by A17,XBOOLE_0:def 3;
suppose
x in id the carrier of G1;
hence contradiction by A13,XBOOLE_0:def 5;
end;
suppose
x in id the carrier of G2;
then [:the carrier of G1,the carrier of G1:] /\ [:the carrier of
G2,the carrier of G2:] is non empty by A13,XBOOLE_0:def 4;
then [:the carrier of G1,the carrier of G1:] meets [:the carrier
of G2,the carrier of G2:];
hence contradiction by A2,ZFMISC_1:104;
end;
end;
end;
x in X5 \/ X7 by A13,XBOOLE_0:def 3;
then x in X5 \/ X7 \/ X8 by XBOOLE_0:def 3;
then x in X5 \/ X7 \/ X8 \/ X6 by XBOOLE_0:def 3;
then
x in [:(the carrier of G1) \/ the carrier of G2, (the carrier of G1
) \/ the carrier of G2:] by ZFMISC_1:98;
then x in [:(the carrier of G1) \/ the carrier of G2, the carrier of
union_of(G1,G2):] by NECKLA_2:def 2;
then x in [:the carrier of union_of(G1,G2), the carrier of union_of(G1,
G2):] by NECKLA_2:def 2;
then x in [:the carrier of union_of(G1,G2),the carrier of union_of(G1,
G2):] \ (the InternalRel of union_of(G1,G2)) by A15,XBOOLE_0:def 5;
then x in (the InternalRel of union_of(G1,G2))` by SUBSET_1:def 4;
then x in (the InternalRel of union_of(G1,G2))` \ id the carrier of
union_of(G1,G2) by A16,XBOOLE_0:def 5;
hence thesis by NECKLACE:def 8;
end;
suppose
x in X2;
then
A18: x in (the InternalRel of G2)` \ id the carrier of G2 by NECKLACE:def 8;
then x in (the InternalRel of G2)` by XBOOLE_0:def 5;
then x in [:the carrier of G2,the carrier of G2:] \ the InternalRel of
G2 by SUBSET_1:def 4;
then
A19: not x in the InternalRel of G2 by XBOOLE_0:def 5;
A20: not x in the InternalRel of union_of(G1,G2)
proof
assume not thesis;
then x in (the InternalRel of G1) \/ the InternalRel of G2 by
NECKLA_2:def 2;
then x in the InternalRel of G1 by A19,XBOOLE_0:def 3;
then [:the carrier of G1,the carrier of G1:] /\ [:the carrier of G2,
the carrier of G2:] is non empty by A18,XBOOLE_0:def 4;
then [:the carrier of G1,the carrier of G1:] meets [:the carrier of
G2,the carrier of G2:];
hence contradiction by A2,ZFMISC_1:104;
end;
A21: not x in id the carrier of union_of(G1,G2)
proof
assume not thesis;
then x in id ((the carrier of G1) \/ the carrier of G2) by
NECKLA_2:def 2;
then
A22: x in (id the carrier of G1) \/ id the carrier of G2 by SYSREL:14;
per cases by A22,XBOOLE_0:def 3;
suppose
x in id the carrier of G2;
hence contradiction by A18,XBOOLE_0:def 5;
end;
suppose
x in id the carrier of G1;
then [:the carrier of G1,the carrier of G1:] /\ [:the carrier of G2
,the carrier of G2:] is non empty by A18,XBOOLE_0:def 4;
then [:the carrier of G1,the carrier of G1:] meets [:the carrier of
G2,the carrier of G2:];
hence contradiction by A2,ZFMISC_1:104;
end;
end;
x in X8 \/ X6 by A18,XBOOLE_0:def 3;
then x in X7 \/ (X8 \/ X6) by XBOOLE_0:def 3;
then x in X7 \/ X8 \/ X6 by XBOOLE_1:4;
then x in X5 \/ (X7 \/ X8 \/ X6) by XBOOLE_0:def 3;
then x in X5 \/ X7 \/ X8 \/ X6 by XBOOLE_1:113;
then
x in [:(the carrier of G1) \/ the carrier of G2, (the carrier of G1
) \/ the carrier of G2:] by ZFMISC_1:98;
then x in [:(the carrier of G1) \/ the carrier of G2, the carrier of
union_of(G1,G2):] by NECKLA_2:def 2;
then x in [:the carrier of union_of(G1,G2), the carrier of union_of(G1,
G2):] by NECKLA_2:def 2;
then x in [:the carrier of union_of(G1,G2),the carrier of union_of(G1,
G2):] \ (the InternalRel of union_of(G1,G2)) by A20,XBOOLE_0:def 5;
then x in (the InternalRel of union_of(G1,G2))` by SUBSET_1:def 4;
then x in (the InternalRel of union_of(G1,G2))` \ id the carrier of
union_of(G1,G2) by A21,XBOOLE_0:def 5;
hence thesis by NECKLACE:def 8;
end;
suppose
x in X3;
then
A23: x in [:the carrier of G1,the carrier of ComplRelStr G2:] by
NECKLACE:def 8;
then
A24: x in [:the carrier of G1,the carrier of G2:] by NECKLACE:def 8;
A25: not x in the InternalRel of union_of(G1,G2)
proof
assume not thesis;
then
A26: x in (the InternalRel of G1) \/ the InternalRel of G2 by NECKLA_2:def 2
;
per cases by A26,XBOOLE_0:def 3;
suppose
A27: x in the InternalRel of G1;
A28: b in the carrier of G2 by A24,ZFMISC_1:87;
b in the carrier of G1 by A27,ZFMISC_1:87;
then b in (the carrier of G1) /\ the carrier of G2 by A28,
XBOOLE_0:def 4;
hence contradiction by A2;
end;
suppose
A29: x in the InternalRel of G2;
A30: a in the carrier of G1 by A23,ZFMISC_1:87;
a in the carrier of G2 by A29,ZFMISC_1:87;
then a in (the carrier of G1) /\ the carrier of G2 by A30,
XBOOLE_0:def 4;
hence contradiction by A2;
end;
end;
A31: not x in id the carrier of union_of(G1,G2)
proof
assume not thesis;
then x in id ((the carrier of G1) \/ the carrier of G2) by
NECKLA_2:def 2;
then
A32: x in (id the carrier of G1) \/ id the carrier of G2 by SYSREL:14;
per cases by A32,XBOOLE_0:def 3;
suppose
A33: x in id the carrier of G1;
A34: b in the carrier of G2 by A24,ZFMISC_1:87;
b in the carrier of G1 by A33,ZFMISC_1:87;
then b in (the carrier of G1) /\ the carrier of G2 by A34,
XBOOLE_0:def 4;
hence contradiction by A2;
end;
suppose
A35: x in id the carrier of G2;
A36: a in the carrier of G1 by A23,ZFMISC_1:87;
a in the carrier of G2 by A35,ZFMISC_1:87;
then a in (the carrier of G1) /\ the carrier of G2 by A36,
XBOOLE_0:def 4;
hence contradiction by A2;
end;
end;
x in X7 \/ X8 by A24,XBOOLE_0:def 3;
then x in X5 \/ (X7 \/ X8) by XBOOLE_0:def 3;
then x in X5 \/ X7 \/ X8 by XBOOLE_1:4;
then x in X5 \/ X7 \/ X8 \/ X6 by XBOOLE_0:def 3;
then x in [:(the carrier of G1) \/ the carrier of G2, (the carrier of
G1) \/ the carrier of G2:] by ZFMISC_1:98;
then x in [:(the carrier of G1) \/ the carrier of G2, the carrier of
union_of(G1,G2):] by NECKLA_2:def 2;
then x in [:the carrier of union_of(G1,G2), the carrier of union_of(G1,
G2):] by NECKLA_2:def 2;
then x in [:the carrier of union_of(G1,G2),the carrier of union_of(G1,
G2):] \ (the InternalRel of union_of(G1,G2)) by A25,XBOOLE_0:def 5;
then x in (the InternalRel of union_of(G1,G2))` by SUBSET_1:def 4;
then x in (the InternalRel of union_of(G1,G2))` \ id the carrier of
union_of(G1,G2) by A31,XBOOLE_0:def 5;
hence thesis by NECKLACE:def 8;
end;
suppose
x in X4;
then
A37: x in [:the carrier of G2,the carrier of ComplRelStr G1:] by
NECKLACE:def 8;
then
A38: x in [:the carrier of G2,the carrier of G1:] by NECKLACE:def 8;
A39: not x in the InternalRel of union_of(G1,G2)
proof
assume not thesis;
then
A40: x in (the InternalRel of G1) \/ the InternalRel of G2 by NECKLA_2:def 2
;
per cases by A40,XBOOLE_0:def 3;
suppose
A41: x in the InternalRel of G1;
A42: a in the carrier of G2 by A37,ZFMISC_1:87;
a in the carrier of G1 by A41,ZFMISC_1:87;
then a in (the carrier of G1) /\ the carrier of G2 by A42,
XBOOLE_0:def 4;
hence contradiction by A2;
end;
suppose
A43: x in the InternalRel of G2;
A44: b in the carrier of G1 by A38,ZFMISC_1:87;
b in the carrier of G2 by A43,ZFMISC_1:87;
then b in (the carrier of G1) /\ the carrier of G2 by A44,
XBOOLE_0:def 4;
hence contradiction by A2;
end;
end;
A45: not x in id the carrier of union_of(G1,G2)
proof
assume not thesis;
then x in id ((the carrier of G1) \/ the carrier of G2) by
NECKLA_2:def 2;
then
A46: x in (id the carrier of G1) \/ id the carrier of G2 by SYSREL:14;
per cases by A46,XBOOLE_0:def 3;
suppose
A47: x in id the carrier of G1;
A48: a in the carrier of G2 by A37,ZFMISC_1:87;
a in the carrier of G1 by A47,ZFMISC_1:87;
then a in (the carrier of G1) /\ the carrier of G2 by A48,
XBOOLE_0:def 4;
hence contradiction by A2;
end;
suppose
A49: x in id the carrier of G2;
A50: b in the carrier of G1 by A38,ZFMISC_1:87;
b in the carrier of G2 by A49,ZFMISC_1:87;
then b in (the carrier of G1) /\ the carrier of G2 by A50,
XBOOLE_0:def 4;
hence contradiction by A2;
end;
end;
x in X7 \/ X8 by A38,XBOOLE_0:def 3;
then x in X5 \/ (X7 \/ X8) by XBOOLE_0:def 3;
then x in X5 \/ X7 \/ X8 by XBOOLE_1:4;
then x in X5 \/ X7 \/ X8 \/ X6 by XBOOLE_0:def 3;
then x in [:(the carrier of G1) \/ the carrier of G2, (the carrier of
G1) \/ the carrier of G2:] by ZFMISC_1:98;
then x in [:(the carrier of G1) \/ the carrier of G2, the carrier of
union_of(G1,G2):] by NECKLA_2:def 2;
then x in [:the carrier of union_of(G1,G2), the carrier of union_of(G1,
G2):] by NECKLA_2:def 2;
then x in [:the carrier of union_of(G1,G2),the carrier of union_of(G1,
G2):] \ (the InternalRel of union_of(G1,G2)) by A39,XBOOLE_0:def 5;
then x in (the InternalRel of union_of(G1,G2))` by SUBSET_1:def 4;
then x in (the InternalRel of union_of(G1,G2))` \ id the carrier of
union_of(G1,G2) by A45,XBOOLE_0:def 5;
hence thesis by NECKLACE:def 8;
end;
end;
the carrier of ComplRelStr union_of(G1,G2) = the carrier of union_of(G1,
G2) by NECKLACE:def 8
.= (the carrier of G1) \/ the carrier of G2 by NECKLA_2:def 2;
hence thesis by A1,A3,RELAT_1:def 2;
end;
theorem Th18:
for G1,G2 being RelStr st the carrier of G1 misses the carrier
of G2 holds ComplRelStr sum_of(G1,G2) = union_of(ComplRelStr G1, ComplRelStr G2
)
proof
let G1,G2 be RelStr;
assume
A1: the carrier of G1 misses the carrier of G2;
set P = the InternalRel of ComplRelStr sum_of(G1,G2), R = the InternalRel of
union_of(ComplRelStr G1,ComplRelStr G2), X1 = the InternalRel of ComplRelStr G1
, X2 = the InternalRel of ComplRelStr G2, X5 = [:the carrier of G1, the carrier
of G1:], X6 = [:the carrier of G2, the carrier of G2:], X7 = [:the carrier of
G1, the carrier of G2:], X8 = [:the carrier of G2, the carrier of G1:];
A2: [:the carrier of sum_of(G1,G2),the carrier of sum_of(G1,G2):] = [:(the
carrier of G1) \/ the carrier of G2, the carrier of sum_of(G1,G2):] by
NECKLA_2:def 3
.= [:(the carrier of G1) \/ the carrier of G2, (the carrier of G1) \/
the carrier of G2:] by NECKLA_2:def 3
.= X5 \/ X7 \/ X8 \/ X6 by ZFMISC_1:98;
A3: for a,b being object holds [a,b] in P iff [a,b] in R
proof
let a,b be object;
set x = [a,b];
thus x in P implies x in R
proof
assume x in P;
then
A4: x in (the InternalRel of sum_of(G1,G2))` \ id (the carrier of sum_of
(G1,G2)) by NECKLACE:def 8;
then x in X5 \/ X7 \/ X8 or x in X6 by A2,XBOOLE_0:def 3;
then
A5: x in X5 \/ X7 or x in X8 or x in X6 by XBOOLE_0:def 3;
x in (the InternalRel of sum_of(G1,G2))` by A4,XBOOLE_0:def 5;
then
x in [:the carrier of sum_of(G1,G2),the carrier of sum_of(G1,G2) :]
\ (the InternalRel of sum_of(G1,G2)) by SUBSET_1:def 4;
then not x in the InternalRel of sum_of(G1,G2) by XBOOLE_0:def 5;
then
A6: not x in (the InternalRel of G1) \/ (the InternalRel of G2) \/ [:
the carrier of G1,the carrier of G2:] \/ [:the carrier of G2,the carrier of G1
:] by NECKLA_2:def 3;
A7: not x in the InternalRel of G1 & not x in the InternalRel of G2 &
not x in [:the carrier of G1,the carrier of G2:] & not x in [:the carrier of G2
,the carrier of G1:]
proof
assume not thesis;
then x in (the InternalRel of G1) \/ the InternalRel of G2 or x in [:
the carrier of G1,the carrier of G2:] or x in [:the carrier of G2,the carrier
of G1:] by XBOOLE_0:def 3;
then x in (the InternalRel of G1) \/ (the InternalRel of G2) \/ [:the
carrier of G1,the carrier of G2:] or x in [:the carrier of G2,the carrier of G1
:] by XBOOLE_0:def 3;
hence contradiction by A6,XBOOLE_0:def 3;
end;
not x in id (the carrier of sum_of(G1,G2)) by A4,XBOOLE_0:def 5;
then not x in id ((the carrier of G1) \/ the carrier of G2) by
NECKLA_2:def 3;
then
A8: not x in id (the carrier of G1) \/ id the carrier of G2 by SYSREL:14;
then
A9: not x in id the carrier of G1 by XBOOLE_0:def 3;
A10: not x in id the carrier of G2 by A8,XBOOLE_0:def 3;
per cases by A5,XBOOLE_0:def 3;
suppose
x in X5;
then x in X5 \ (the InternalRel of G1) by A7,XBOOLE_0:def 5;
then x in (the InternalRel of G1)` by SUBSET_1:def 4;
then x in (the InternalRel of G1)` \ id the carrier of G1 by A9,
XBOOLE_0:def 5;
then x in X1 by NECKLACE:def 8;
then x in X1 \/ X2 by XBOOLE_0:def 3;
hence thesis by NECKLA_2:def 2;
end;
suppose
x in X7;
hence thesis by A7;
end;
suppose
x in X8;
hence thesis by A7;
end;
suppose
x in X6;
then x in X6 \ (the InternalRel of G2) by A7,XBOOLE_0:def 5;
then x in (the InternalRel of G2)` by SUBSET_1:def 4;
then x in (the InternalRel of G2)` \ id the carrier of G2 by A10,
XBOOLE_0:def 5;
then x in X2 by NECKLACE:def 8;
then x in X1 \/ X2 by XBOOLE_0:def 3;
hence thesis by NECKLA_2:def 2;
end;
end;
assume x in R;
then
A11: x in (the InternalRel of ComplRelStr G1) \/ the InternalRel of
ComplRelStr G2 by NECKLA_2:def 2;
per cases by A11,XBOOLE_0:def 3;
suppose
x in the InternalRel of ComplRelStr G1;
then
A12: x in (the InternalRel of G1)` \ id the carrier of G1 by NECKLACE:def 8;
then
A13: not x in id the carrier of G1 by XBOOLE_0:def 5;
A14: not x in id (the carrier of sum_of(G1,G2))
proof
assume not thesis;
then x in id ((the carrier of G1) \/ the carrier of G2) by
NECKLA_2:def 3;
then x in id (the carrier of G1) \/ id the carrier of G2 by SYSREL:14;
then x in id the carrier of G2 by A13,XBOOLE_0:def 3;
then
A15: a in the carrier of G2 by ZFMISC_1:87;
a in the carrier of G1 by A12,ZFMISC_1:87;
then (the carrier of G1) /\ the carrier of G2 is non empty by A15,
XBOOLE_0:def 4;
hence contradiction by A1;
end;
x in (the InternalRel of G1)` by A12,XBOOLE_0:def 5;
then x in [:the carrier of G1,the carrier of G1:] \ the InternalRel of
G1 by SUBSET_1:def 4;
then
A16: not x in the InternalRel of G1 by XBOOLE_0:def 5;
A17: not x in the InternalRel of sum_of(G1,G2)
proof
assume not thesis;
then x in (the InternalRel of G1) \/ (the InternalRel of G2) \/ X7 \/
X8 by NECKLA_2:def 3;
then x in (the InternalRel of G1) \/ (the InternalRel of G2) \/ X7 or
x in X8 by XBOOLE_0:def 3;
then
A18: x in (the InternalRel of G1) \/ the InternalRel of G2 or x in X7
or x in X8 by XBOOLE_0:def 3;
per cases by A16,A18,XBOOLE_0:def 3;
suppose
A19: x in the InternalRel of G2;
A20: a in the carrier of G1 by A12,ZFMISC_1:87;
a in the carrier of G2 by A19,ZFMISC_1:87;
then (the carrier of G1) /\ the carrier of G2 is non empty by A20,
XBOOLE_0:def 4;
hence contradiction by A1;
end;
suppose
A21: x in X7;
A22: b in the carrier of G1 by A12,ZFMISC_1:87;
b in the carrier of G2 by A21,ZFMISC_1:87;
then (the carrier of G1) /\ the carrier of G2 is non empty by A22,
XBOOLE_0:def 4;
hence contradiction by A1;
end;
suppose
A23: x in X8;
A24: a in the carrier of G1 by A12,ZFMISC_1:87;
a in the carrier of G2 by A23,ZFMISC_1:87;
then (the carrier of G1) /\ the carrier of G2 is non empty by A24,
XBOOLE_0:def 4;
hence contradiction by A1;
end;
end;
x in X5 \/ (X7 \/ X8 \/ X6) by A12,XBOOLE_0:def 3;
then
x in [:the carrier of sum_of(G1,G2),the carrier of sum_of(G1,G2) :]
by A2,XBOOLE_1:113;
then
x in [:the carrier of sum_of(G1,G2),the carrier of sum_of(G1,G2) :]
\ (the InternalRel of sum_of(G1,G2)) by A17,XBOOLE_0:def 5;
then x in (the InternalRel of sum_of(G1,G2))` by SUBSET_1:def 4;
then x in (the InternalRel of sum_of(G1,G2))` \ id (the carrier of
sum_of(G1,G2)) by A14,XBOOLE_0:def 5;
hence thesis by NECKLACE:def 8;
end;
suppose
x in the InternalRel of ComplRelStr G2;
then
A25: x in (the InternalRel of G2)` \ id the carrier of G2 by NECKLACE:def 8;
then
A26: not x in id the carrier of G2 by XBOOLE_0:def 5;
A27: not x in id (the carrier of sum_of(G1,G2))
proof
assume not thesis;
then x in id ((the carrier of G1) \/ the carrier of G2) by
NECKLA_2:def 3;
then x in id (the carrier of G1) \/ id the carrier of G2 by SYSREL:14;
then x in id the carrier of G1 by A26,XBOOLE_0:def 3;
then
A28: b in the carrier of G1 by ZFMISC_1:87;
b in the carrier of G2 by A25,ZFMISC_1:87;
then (the carrier of G1) /\ the carrier of G2 is non empty by A28,
XBOOLE_0:def 4;
hence contradiction by A1;
end;
x in (the InternalRel of G2)` by A25,XBOOLE_0:def 5;
then x in [:the carrier of G2,the carrier of G2:] \ the InternalRel of
G2 by SUBSET_1:def 4;
then
A29: not x in the InternalRel of G2 by XBOOLE_0:def 5;
A30: not x in the InternalRel of sum_of(G1,G2)
proof
assume not thesis;
then x in (the InternalRel of G1) \/ (the InternalRel of G2) \/ X7 \/
X8 by NECKLA_2:def 3;
then x in (the InternalRel of G1) \/ (the InternalRel of G2) \/ X7 or
x in X8 by XBOOLE_0:def 3;
then
A31: x in (the InternalRel of G1) \/ the InternalRel of G2 or x in X7
or x in X8 by XBOOLE_0:def 3;
per cases by A29,A31,XBOOLE_0:def 3;
suppose
A32: x in the InternalRel of G1;
A33: a in the carrier of G2 by A25,ZFMISC_1:87;
a in the carrier of G1 by A32,ZFMISC_1:87;
then (the carrier of G1) /\ the carrier of G2 is non empty by A33,
XBOOLE_0:def 4;
hence contradiction by A1;
end;
suppose
A34: x in X7;
A35: a in the carrier of G2 by A25,ZFMISC_1:87;
a in the carrier of G1 by A34,ZFMISC_1:87;
then (the carrier of G1) /\ the carrier of G2 is non empty by A35,
XBOOLE_0:def 4;
hence contradiction by A1;
end;
suppose
A36: x in X8;
A37: b in the carrier of G2 by A25,ZFMISC_1:87;
b in the carrier of G1 by A36,ZFMISC_1:87;
then (the carrier of G1) /\ the carrier of G2 is non empty by A37,
XBOOLE_0:def 4;
hence contradiction by A1;
end;
end;
x in [:the carrier of sum_of(G1,G2),the carrier of sum_of(G1,G2):]
by A2,A25,XBOOLE_0:def 3;
then x in [:the carrier of sum_of(G1,G2),the carrier of sum_of(G1,G2 )
:] \ (the InternalRel of sum_of(G1,G2)) by A30,XBOOLE_0:def 5;
then x in (the InternalRel of sum_of(G1,G2))` by SUBSET_1:def 4;
then x in (the InternalRel of sum_of(G1,G2))` \ id (the carrier of
sum_of(G1,G2)) by A27,XBOOLE_0:def 5;
hence thesis by NECKLACE:def 8;
end;
end;
A38: the carrier of union_of(ComplRelStr G1, ComplRelStr G2) = (the carrier
of ComplRelStr G1) \/ (the carrier of ComplRelStr G2) by NECKLA_2:def 2
.= (the carrier of G1) \/ the carrier of ComplRelStr G2 by NECKLACE:def 8
.= (the carrier of G1) \/ the carrier of G2 by NECKLACE:def 8;
the carrier of ComplRelStr sum_of(G1,G2) = the carrier of sum_of(G1,G2)
by NECKLACE:def 8
.= (the carrier of G1) \/ the carrier of G2 by NECKLA_2:def 3;
hence thesis by A38,A3,RELAT_1:def 2;
end;
theorem
for G being RelStr, H being full SubRelStr of G holds the InternalRel
of ComplRelStr H = (the InternalRel of ComplRelStr G)|_2 the carrier of
ComplRelStr H
proof
let G be RelStr, H be full SubRelStr of G;
set IH = the InternalRel of H, ICmpH = the InternalRel of ComplRelStr H, cH
= the carrier of H, IG = the InternalRel of G, cG = the carrier of G, ICmpG =
the InternalRel of ComplRelStr G;
A1: ICmpH = IH` \ id cH by NECKLACE:def 8
.= [:cH,cH:] \ IH \ id cH by SUBSET_1:def 4;
A2: ICmpG = IG` \ id cG by NECKLACE:def 8
.= [:cG,cG:] \ IG \ id cG by SUBSET_1:def 4;
A3: cH c= cG by YELLOW_0:def 13;
ICmpG |_2 the carrier of ComplRelStr H = ICmpG |_2 cH by NECKLACE:def 8
.= ([:cG,cG:] \ IG) /\ [:cH,cH:] \ id cG /\ [:cH,cH:] by A2,XBOOLE_1:50
.= ([:cG,cG:] /\ [:cH,cH:]) \ (IG /\ [:cH,cH:]) \ (id cG /\ [:cH,cH:])
by XBOOLE_1:50
.= ([:cG,cG:] /\ [:cH,cH:]) \ (IG /\ [:cH,cH:]) \ (id cG)|cH by Th1
.= ([:cG,cG:] /\ [:cH,cH:]) \ IG|_2 cH \ id cH by A3,FUNCT_3:1
.= ([:cG,cG:] /\ [:cH,cH:]) \ IH \ id cH by YELLOW_0:def 14
.= [:cG /\ cH, cG /\ cH:] \ IH \ id cH by ZFMISC_1:100
.= [:cH, cG /\ cH:] \ IH \ id cH by A3,XBOOLE_1:28
.= ICmpH by A1,A3,XBOOLE_1:28;
hence thesis;
end;
theorem Th20:
for G being non empty irreflexive RelStr, x being Element of G,
x9 being Element of ComplRelStr G st x = x9 holds ComplRelStr (subrelstr ([#]G
\ {x})) = subrelstr ([#](ComplRelStr G) \ {x9})
proof
let G be non empty irreflexive RelStr, x be Element of G, x9 be Element of
ComplRelStr G;
assume
A1: x = x9;
set R = subrelstr ([#]G \ {x}), cR = the carrier of R, cG = the carrier of G;
A2: [#]ComplRelStr G = cG by NECKLACE:def 8;
A3: [:(cG \ {x}),(cG \ {x}):] = [:cR,([#]G \ {x}):] by YELLOW_0:def 15
.= [:cR,cR:] by YELLOW_0:def 15;
A4: cR c= cG by YELLOW_0:def 13;
A5: the InternalRel of subrelstr ([#](ComplRelStr G) \ {x9}) = (the
InternalRel of ComplRelStr G)|_2 the carrier of subrelstr ([#](ComplRelStr G) \
{x9}) by YELLOW_0:def 14
.= (the InternalRel of ComplRelStr G)|_2 (cG \ {x}) by A1,A2,
YELLOW_0:def 15
.= ((the InternalRel of G)` \ id cG ) /\ [:(cG \ {x}),(cG \ {x}):] by
NECKLACE:def 8
.= ( [:cR,cR:] /\ (the InternalRel of G)` ) \ id cG by A3,XBOOLE_1:49
.= ( [:cR,cR:] /\ ([:cG,cG:] \ the InternalRel of G) ) \ id cG by
SUBSET_1:def 4
.= ( ([:cR,cR:] /\ [:cG,cG:]) \ the InternalRel of G) \ id cG by
XBOOLE_1:49
.= ([:cR,cR:] \ (the InternalRel of G)) \ id cG by A4,XBOOLE_1:28
,ZFMISC_1:96;
A6: the InternalRel of ComplRelStr R = (the InternalRel of R)` \ id cR by
NECKLACE:def 8
.= [:cR,cR:] \ (the InternalRel of R) \ id cR by SUBSET_1:def 4
.= [:cR,cR:] \ ( (the InternalRel of G)|_2 cR ) \id cR by YELLOW_0:def 14
.= ( ([:cR,cR:] \ (the InternalRel of G)) \/ ([:cR,cR:] \ [:cR,cR:]) ) \
id cR by XBOOLE_1:54
.= ( ([:cR,cR:] \ (the InternalRel of G)) \/ {}) \ id cR by XBOOLE_1:37
.= ([:cR,cR:] \ (the InternalRel of G)) \ id cR;
A7: [:cR,cR:] = [:[#]G,([#]G \ {x}):] \ [:{x},([#]G \ {x}):] by A3,ZFMISC_1:102
.= [:[#]G,[#]G:] \ [:[#]G,{x}:] \ [:{x},([#]G\{x}):] by ZFMISC_1:102
.= [:cG,cG:] \ [:cG,{x}:] \ ([:{x},cG:] \ [:{x},{x}:]) by ZFMISC_1:102
.= ( ([:cG,cG:] \ [:cG,{x}:]) \ [:{x},cG:] ) \/ ([:cG,cG:] \ [:cG,{x}:])
/\ [:{x},{x}:] by XBOOLE_1:52
.= ([:cG,cG:] \ ([:cG,{x}:] \/ [:{x},cG:]) ) \/ ([:cG,cG:] \ [:cG,{x}:])
/\ [:{x},{x}:] by XBOOLE_1:41;
A8: the InternalRel of subrelstr ([#](ComplRelStr G) \ {x9}) = the
InternalRel of ComplRelStr R
proof
thus the InternalRel of subrelstr ([#](ComplRelStr G) \ {x9}) c= the
InternalRel of ComplRelStr R
proof
let a be object;
assume
A9: a in the InternalRel of subrelstr ([#](ComplRelStr G) \ {x9});
then
A10: not a in id cG by A5,XBOOLE_0:def 5;
A11: not a in id cR
proof
assume
A12: not thesis;
then consider x2,y2 being object such that
A13: a = [x2,y2] and
A14: x2 in cR and
y2 in cR by RELSET_1:2;
A15: x2 in cG \ {x} by A14,YELLOW_0:def 15;
x2 = y2 by A12,A13,RELAT_1:def 10;
hence contradiction by A10,A13,A15,RELAT_1:def 10;
end;
a in ([:cR,cR:] \ (the InternalRel of G)) by A5,A9,XBOOLE_0:def 5;
hence thesis by A6,A11,XBOOLE_0:def 5;
end;
let a be object;
assume
A16: a in the InternalRel of ComplRelStr R;
then not a in id cR by A6,XBOOLE_0:def 5;
then not a in id (cG \ {x}) by YELLOW_0:def 15;
then
A17: not a in (id cG \ id {x}) by SYSREL:14;
per cases by A17,XBOOLE_0:def 5;
suppose
A18: not a in id cG;
a in ([:cR,cR:] \ (the InternalRel of G)) by A6,A16,XBOOLE_0:def 5;
hence thesis by A5,A18,XBOOLE_0:def 5;
end;
suppose
a in id {x};
then
A19: a in {[x,x]} by SYSREL:13;
thus thesis
proof
per cases by A7,A6,A16,XBOOLE_0:def 3;
suppose
A20: a in [:cG,cG:] \ ([:cG,{x}:] \/ [:{x},cG:]);
x in {x} by TARSKI:def 1;
then
A21: [x,x] in [:{x},cG:] by ZFMISC_1:87;
not a in ([:cG,{x}:] \/ [:{x},cG:]) by A20,XBOOLE_0:def 5;
then not a in [:{x}, cG:] by XBOOLE_0:def 3;
hence thesis by A19,A21,TARSKI:def 1;
end;
suppose
A22: a in ([:cG,cG:] \ [:cG,{x}:]) /\ [:{x},{x}:];
x in {x} by TARSKI:def 1;
then
A23: [x,x] in [:cG,{x}:] by ZFMISC_1:87;
a in [:cG,cG:] \ [:cG,{x}:] by A22,XBOOLE_0:def 4;
then not a in [:cG,{x}:] by XBOOLE_0:def 5;
hence thesis by A19,A23,TARSKI:def 1;
end;
end;
end;
end;
the carrier of ComplRelStr (subrelstr ([#]G \ {x})) = the carrier of (
subrelstr ([#]G \ {x})) by NECKLACE:def 8
.= (the carrier of G) \ {x} by YELLOW_0:def 15
.= [#](ComplRelStr G) \ {x9} by A1,NECKLACE:def 8
.= the carrier of subrelstr ([#](ComplRelStr G) \ {x9}) by YELLOW_0:def 15;
hence thesis by A8;
end;
begin :: Another facts relating to operation 'embeds'
registration
cluster trivial strict -> N-free for non empty RelStr;
correctness
proof
set Y = Necklace 4;
let R be non empty RelStr;
assume R is trivial strict;
then consider y be object such that
A1: the carrier of R = {y} by GROUP_6:def 2;
assume not R is N-free;
then R embeds Y by NECKLA_2:def 1;
then consider f being Function of Y,R such that
A2: f is one-to-one and
for x,y being Element of Y holds [x,y] in the InternalRel of Y iff [ f
.x,f.y] in the InternalRel of R;
A3: dom f = the carrier of Y by FUNCT_2:def 1
.= {0,1,2,3} by NECKLACE:1,20;
then
A4: 1 in dom f by ENUMSET1:def 2;
then f.1 in {y} by A1,PARTFUN1:4;
then
A5: f.1 = y by TARSKI:def 1;
A6: 0 in dom f by A3,ENUMSET1:def 2;
then f.0 in {y} by A1,PARTFUN1:4;
then f.0 = y by TARSKI:def 1;
hence contradiction by A2,A6,A4,A5,FUNCT_1:def 4;
end;
end;
theorem
for R being reflexive antisymmetric RelStr, S being RelStr holds (ex f
being Function of R,S st for x,y being Element of R holds [x,y] in the
InternalRel of R iff [f.x,f.y] in the InternalRel of S) iff S embeds R
proof
let R being reflexive antisymmetric RelStr, S being RelStr;
A1: now
assume ex f being Function of R,S st for x,y being Element of R holds [x,
y] in the InternalRel of R iff [f.x,f.y] in the InternalRel of S;
then consider f being Function of R,S such that
A2: for x,y being Element of R holds [x,y] in the InternalRel of R iff
[f.x,f.y] in the InternalRel of S;
for x1,x2 being object st x1 in dom f & x2 in dom f & f.x1 = f.x2 holds
x1 = x2
proof
let x1,x2 be object;
assume that
A3: x1 in dom f and
A4: x2 in dom f and
A5: f.x1 = f.x2;
reconsider x1,x2 as Element of R by A3,A4;
A6: the InternalRel of R is_reflexive_in the carrier of R by ORDERS_2:def 2;
then [x2,x2] in the InternalRel of R by A3;
then [f.x2,f.x1] in the InternalRel of S by A2,A5;
then [x2,x1] in the InternalRel of R by A2;
then
A7: x2 <= x1 by ORDERS_2:def 5;
[x1,x1] in the InternalRel of R by A3,A6;
then [f.x1,f.x2] in the InternalRel of S by A2,A5;
then [x1,x2] in the InternalRel of R by A2;
then x1 <= x2 by ORDERS_2:def 5;
hence thesis by A7,ORDERS_2:2;
end;
then f is one-to-one by FUNCT_1:def 4;
hence S embeds R by A2;
end;
thus thesis by A1;
end;
theorem Th22:
for G being non empty RelStr, H being non empty full SubRelStr
of G holds G embeds H
proof
let G be non empty RelStr;
let H be non empty full SubRelStr of G;
reconsider f = id the carrier of H as Function of the carrier of H, the
carrier of H;
A1: dom f = the carrier of H;
A2: the carrier of H c= the carrier of G by YELLOW_0:def 13;
for x being object st x in the carrier of H holds f.x in the carrier of G
proof
let x be object;
assume x in the carrier of H;
then f.x in the carrier of H by FUNCT_1:17;
hence thesis by A2;
end;
then reconsider f = id the carrier of H as Function of the carrier of H, the
carrier of G by A1,FUNCT_2:3;
reconsider f as Function of H,G;
for x,y being Element of H holds [x,y] in the InternalRel of H iff [f.x,
f.y] in the InternalRel of G
proof
set IH = the InternalRel of H, IG = the InternalRel of G, cH = the carrier
of H;
let x,y be Element of H;
thus [x,y] in IH implies [f.x,f.y] in IG
proof
assume [x,y] in IH;
then [x,y] in IG |_2 cH by YELLOW_0:def 14;
hence thesis by XBOOLE_0:def 4;
end;
assume [f.x,f.y] in IG;
then [x,y] in IG |_2 cH by XBOOLE_0:def 4;
hence thesis by YELLOW_0:def 14;
end;
hence thesis;
end;
theorem Th23:
for G being non empty RelStr, H being non empty full SubRelStr
of G st G is N-free holds H is N-free
proof
let G be non empty RelStr, H be non empty full SubRelStr of G;
assume
A1: G is N-free;
A2: G embeds H by Th22;
assume not thesis;
then H embeds Necklace 4 by NECKLA_2:def 1;
then G embeds Necklace 4 by A2,NECKLACE:12;
hence contradiction by A1,NECKLA_2:def 1;
end;
theorem Th24:
for G being non empty irreflexive RelStr holds G embeds Necklace
4 iff ComplRelStr G embeds Necklace 4
proof
let G be non empty irreflexive RelStr;
set N4 = Necklace 4, CmpN4 = ComplRelStr Necklace 4, CmpG = ComplRelStr G;
A1: the carrier of CmpG = the carrier of G by NECKLACE:def 8;
A2: the carrier of Necklace 4 = {0,1,2,3} by NECKLACE:1,20;
then
A3: 0 in the carrier of N4 by ENUMSET1:def 2;
A4: the carrier of CmpN4 = the carrier of N4 by NECKLACE:def 8;
thus G embeds N4 implies CmpG embeds N4
proof
CmpN4,N4 are_isomorphic by NECKLACE:29,WAYBEL_1:6;
then consider g being Function of CmpN4,N4 such that
A5: g is isomorphic by WAYBEL_1:def 8;
assume G embeds Necklace 4;
then consider f being Function of N4,G such that
A6: f is one-to-one and
A7: for x,y being Element of N4 holds [x,y] in the InternalRel of N4
iff [f.x,f.y] in the InternalRel of G;
reconsider h = f*g as Function of CmpN4,G;
A8: g is one-to-one monotone by A5,WAYBEL_0:def 38;
A9: for x,y being Element of CmpN4 holds [x,y] in the InternalRel of
CmpN4 iff [h.x,h.y] in the InternalRel of G
proof
let x,y be Element of CmpN4;
thus [x,y] in the InternalRel of CmpN4 implies [h.x,h.y] in the
InternalRel of G
proof
assume [x,y] in the InternalRel of CmpN4;
then x <= y by ORDERS_2:def 5;
then g.x <= g.y by A8,WAYBEL_1:def 2;
then [g.x,g.y] in the InternalRel of N4 by ORDERS_2:def 5;
then [f.(g.x),f.(g.y)] in the InternalRel of G by A7;
then [(f*g).x,f.(g.y)] in the InternalRel of G by FUNCT_2:15;
hence thesis by FUNCT_2:15;
end;
assume [h.x,h.y] in the InternalRel of G;
then [f.(g.x),h.y] in the InternalRel of G by FUNCT_2:15;
then [f.(g.x),f.(g.y)] in the InternalRel of G by FUNCT_2:15;
then [g.x,g.y] in the InternalRel of N4 by A7;
then g.x <= g.y by ORDERS_2:def 5;
then x <= y by A5,WAYBEL_0:66;
hence thesis by ORDERS_2:def 5;
end;
A10: 0 in the carrier of CmpN4 by A2,A4,ENUMSET1:def 2;
A11: 1 in the carrier of CmpN4 by A2,A4,ENUMSET1:def 2;
A12: dom h = the carrier of CmpN4 by FUNCT_2:def 1;
A13: [h.0,h.1] in the InternalRel of CmpG
proof
assume
A14: not thesis;
[h.0,h.1] in the InternalRel of G
proof
h.0 in the carrier of G & h.1 in the carrier of G by A10,A11,FUNCT_2:5;
then [h.0,h.1] in [:the carrier of G,the carrier of G:] by ZFMISC_1:87;
then
[h.0,h.1] in id (the carrier of G) \/ (the InternalRel of G) \/ (
the InternalRel of CmpG) by Th14;
then
A15: [h.0,h.1] in id (the carrier of G) \/ (the InternalRel of G) or [
h.0,h.1] in the InternalRel of CmpG by XBOOLE_0:def 3;
assume not thesis;
then [h.0,h.1] in id (the carrier of G) by A14,A15,XBOOLE_0:def 3;
then h.0 = h.1 by RELAT_1:def 10;
hence contradiction by A6,A8,A12,A10,A11,FUNCT_1:def 4;
end;
then
A16: [0,1] in the InternalRel of CmpN4 by A9,A10,A11;
[0,1] in the InternalRel of N4 by ENUMSET1:def 4,NECKLA_2:2;
then [0,1] in (the InternalRel of N4) /\ (the InternalRel of CmpN4) by
A16,XBOOLE_0:def 4;
then the InternalRel of N4 meets the InternalRel of CmpN4;
hence thesis by Th12;
end;
A17: 2 in the carrier of CmpN4 by A2,A4,ENUMSET1:def 2;
A18: [h.1,h.2] in the InternalRel of CmpG
proof
assume
A19: not thesis;
[h.1,h.2] in the InternalRel of G
proof
h.1 in the carrier of G & h.2 in the carrier of G by A11,A17,FUNCT_2:5;
then [h.1,h.2] in [:the carrier of G,the carrier of G:] by ZFMISC_1:87;
then
[h.1,h.2] in id (the carrier of G) \/ (the InternalRel of G) \/ (
the InternalRel of CmpG) by Th14;
then
A20: [h.1,h.2] in id (the carrier of G) \/ (the InternalRel of G) or [
h.1,h.2] in the InternalRel of CmpG by XBOOLE_0:def 3;
assume not thesis;
then [h.1,h.2] in id (the carrier of G) by A19,A20,XBOOLE_0:def 3;
then h.1 = h.2 by RELAT_1:def 10;
hence contradiction by A6,A8,A12,A11,A17,FUNCT_1:def 4;
end;
then
A21: [1,2] in the InternalRel of CmpN4 by A9,A11,A17;
[1,2] in the InternalRel of N4 by ENUMSET1:def 4,NECKLA_2:2;
then [1,2] in (the InternalRel of N4) /\ (the InternalRel of CmpN4) by
A21,XBOOLE_0:def 4;
then the InternalRel of N4 meets the InternalRel of CmpN4;
hence thesis by Th12;
end;
A22: 3 in the carrier of CmpN4 by A2,A4,ENUMSET1:def 2;
A23: [h.2,h.3] in the InternalRel of CmpG
proof
assume
A24: not thesis;
[h.2,h.3] in the InternalRel of G
proof
h.2 in the carrier of G & h.3 in the carrier of G by A17,A22,FUNCT_2:5;
then [h.2,h.3] in [:the carrier of G,the carrier of G:] by ZFMISC_1:87;
then [h.2,h.3] in id (the carrier of G) \/ (the InternalRel of G) \/
(the InternalRel of CmpG) by Th14;
then
A25: [h.2,h.3] in id (the carrier of G) \/ (the InternalRel of G) or
[h.2,h.3] in the InternalRel of CmpG by XBOOLE_0:def 3;
assume not thesis;
then [h.2,h.3] in id (the carrier of G) by A24,A25,XBOOLE_0:def 3;
then h.2 = h.3 by RELAT_1:def 10;
hence contradiction by A6,A8,A12,A17,A22,FUNCT_1:def 4;
end;
then
A26: [2,3] in the InternalRel of CmpN4 by A9,A17,A22;
[2,3] in the InternalRel of N4 by ENUMSET1:def 4,NECKLA_2:2;
then [2,3] in (the InternalRel of N4) /\ (the InternalRel of CmpN4) by
A26,XBOOLE_0:def 4;
then the InternalRel of N4 meets the InternalRel of CmpN4;
hence thesis by Th12;
end;
[3,1] in the InternalRel of CmpN4 by Th11,ENUMSET1:def 4;
then
A27: [h.3,h.1] in the InternalRel of G by A9,A11,A22;
[1,3] in the InternalRel of CmpN4 by Th11,ENUMSET1:def 4;
then
A28: [h.1,h.3] in the InternalRel of G by A9,A11,A22;
[3,0] in the InternalRel of CmpN4 by Th11,ENUMSET1:def 4;
then
A29: [h.3,h.0] in the InternalRel of G by A9,A10,A22;
[0,3] in the InternalRel of CmpN4 by Th11,ENUMSET1:def 4;
then
A30: [h.0,h.3] in the InternalRel of G by A9,A10,A22;
A31: [h.1,h.0] in the InternalRel of CmpG
proof
assume
A32: not thesis;
[h.1,h.0] in the InternalRel of G
proof
h.0 in the carrier of G & h.1 in the carrier of G by A10,A11,FUNCT_2:5;
then [h.1,h.0] in [:the carrier of G,the carrier of G:] by ZFMISC_1:87;
then
[h.1,h.0] in id (the carrier of G) \/ (the InternalRel of G) \/ (
the InternalRel of CmpG) by Th14;
then
A33: [h.1,h.0] in id (the carrier of G) \/ (the InternalRel of G) or [
h.1,h.0] in the InternalRel of CmpG by XBOOLE_0:def 3;
assume not thesis;
then [h.1,h.0] in id (the carrier of G) by A32,A33,XBOOLE_0:def 3;
then h.0 = h.1 by RELAT_1:def 10;
hence contradiction by A6,A8,A12,A10,A11,FUNCT_1:def 4;
end;
then
A34: [1,0] in the InternalRel of CmpN4 by A9,A10,A11;
[1,0] in the InternalRel of N4 by ENUMSET1:def 4,NECKLA_2:2;
then [1,0] in (the InternalRel of N4) /\ (the InternalRel of CmpN4) by
A34,XBOOLE_0:def 4;
then the InternalRel of N4 meets the InternalRel of CmpN4;
hence thesis by Th12;
end;
A35: [h.2,h.1] in the InternalRel of CmpG
proof
assume
A36: not thesis;
[h.2,h.1] in the InternalRel of G
proof
h.1 in the carrier of G & h.2 in the carrier of G by A11,A17,FUNCT_2:5;
then [h.2,h.1] in [:the carrier of G,the carrier of G:] by ZFMISC_1:87;
then
[h.2,h.1] in id (the carrier of G) \/ (the InternalRel of G) \/ (
the InternalRel of CmpG) by Th14;
then
A37: [h.2,h.1] in id (the carrier of G) \/ (the InternalRel of G) or [
h.2,h.1] in the InternalRel of CmpG by XBOOLE_0:def 3;
assume not thesis;
then [h.2,h.1] in id (the carrier of G) by A36,A37,XBOOLE_0:def 3;
then h.1 = h.2 by RELAT_1:def 10;
hence contradiction by A6,A8,A12,A11,A17,FUNCT_1:def 4;
end;
then
A38: [2,1] in the InternalRel of CmpN4 by A9,A11,A17;
[2,1] in the InternalRel of N4 by ENUMSET1:def 4,NECKLA_2:2;
then [2,1] in (the InternalRel of N4) /\ (the InternalRel of CmpN4) by
A38,XBOOLE_0:def 4;
then the InternalRel of N4 meets the InternalRel of CmpN4;
hence thesis by Th12;
end;
A39: [h.3,h.2] in the InternalRel of CmpG
proof
assume
A40: not thesis;
[h.3,h.2] in the InternalRel of G
proof
h.2 in the carrier of G & h.3 in the carrier of G by A17,A22,FUNCT_2:5;
then [h.3,h.2] in [:the carrier of G,the carrier of G:] by ZFMISC_1:87;
then [h.3,h.2] in id (the carrier of G) \/ (the InternalRel of G) \/
(the InternalRel of CmpG) by Th14;
then
A41: [h.3,h.2] in id (the carrier of G) \/ (the InternalRel of G) or
[h.3,h.2] in the InternalRel of CmpG by XBOOLE_0:def 3;
assume not thesis;
then [h.3,h.2] in id (the carrier of G) by A40,A41,XBOOLE_0:def 3;
then h.2 = h.3 by RELAT_1:def 10;
hence contradiction by A6,A8,A12,A17,A22,FUNCT_1:def 4;
end;
then
A42: [3,2] in the InternalRel of CmpN4 by A9,A17,A22;
[3,2] in the InternalRel of N4 by ENUMSET1:def 4,NECKLA_2:2;
then [3,2] in (the InternalRel of N4) /\ (the InternalRel of CmpN4) by
A42,XBOOLE_0:def 4;
then the InternalRel of N4 meets the InternalRel of CmpN4;
hence thesis by Th12;
end;
[2,0] in the InternalRel of CmpN4 by Th11,ENUMSET1:def 4;
then
A43: [h.2,h.0] in the InternalRel of G by A9,A10,A17;
[0,2] in the InternalRel of CmpN4 by Th11,ENUMSET1:def 4;
then
A44: [h.0,h.2] in the InternalRel of G by A9,A10,A17;
for x,y being Element of N4 holds [x,y] in the InternalRel of N4 iff
[h.x,h.y] in the InternalRel of CmpG
proof
let x,y be Element of N4;
thus [x,y] in the InternalRel of N4 implies [h.x,h.y] in the InternalRel
of CmpG
proof
assume
A45: [x,y] in the InternalRel of N4;
per cases by A45,ENUMSET1:def 4,NECKLA_2:2;
suppose
A46: [x,y] = [0,1];
then x = 0 by XTUPLE_0:1;
hence thesis by A13,A46,XTUPLE_0:1;
end;
suppose
A47: [x,y] = [1,0];
then x = 1 by XTUPLE_0:1;
hence thesis by A31,A47,XTUPLE_0:1;
end;
suppose
A48: [x,y] = [1,2];
then x = 1 by XTUPLE_0:1;
hence thesis by A18,A48,XTUPLE_0:1;
end;
suppose
A49: [x,y] = [2,1];
then x = 2 by XTUPLE_0:1;
hence thesis by A35,A49,XTUPLE_0:1;
end;
suppose
A50: [x,y] = [2,3];
then x = 2 by XTUPLE_0:1;
hence thesis by A23,A50,XTUPLE_0:1;
end;
suppose
A51: [x,y] = [3,2];
then x = 3 by XTUPLE_0:1;
hence thesis by A39,A51,XTUPLE_0:1;
end;
end;
assume
A52: [h.x,h.y] in the InternalRel of CmpG;
per cases by A2,ENUMSET1:def 2;
suppose
A53: x = 0 & y = 0;
then h.0 in the carrier of CmpG by A52,ZFMISC_1:87;
hence thesis by A52,A53,NECKLACE:def 5;
end;
suppose
x = 0 & y = 1;
hence thesis by ENUMSET1:def 4,NECKLA_2:2;
end;
suppose
x = 0 & y = 2;
then [h.0,h.2] in (the InternalRel of G) /\ the InternalRel of CmpG
by A44,A52,XBOOLE_0:def 4;
then the InternalRel of G meets the InternalRel of CmpG;
hence thesis by Th12;
end;
suppose
x = 0 & y = 3;
then [h.0,h.3] in (the InternalRel of G) /\ the InternalRel of CmpG
by A30,A52,XBOOLE_0:def 4;
then the InternalRel of G meets the InternalRel of CmpG;
hence thesis by Th12;
end;
suppose
x = 1 & y = 0;
hence thesis by ENUMSET1:def 4,NECKLA_2:2;
end;
suppose
A54: x = 1 & y = 1;
then h.1 in the carrier of CmpG by A52,ZFMISC_1:87;
hence thesis by A52,A54,NECKLACE:def 5;
end;
suppose
x = 1 & y = 2;
hence thesis by ENUMSET1:def 4,NECKLA_2:2;
end;
suppose
x = 1 & y = 3;
then [h.1,h.3] in (the InternalRel of G) /\ the InternalRel of CmpG
by A28,A52,XBOOLE_0:def 4;
then the InternalRel of G meets the InternalRel of CmpG;
hence thesis by Th12;
end;
suppose
x = 2 & y = 0;
then [h.2,h.0] in (the InternalRel of G) /\ the InternalRel of CmpG
by A43,A52,XBOOLE_0:def 4;
then the InternalRel of G meets the InternalRel of CmpG;
hence thesis by Th12;
end;
suppose
x = 2 & y = 1;
hence thesis by ENUMSET1:def 4,NECKLA_2:2;
end;
suppose
A55: x = 2 & y = 2;
then h.2 in the carrier of CmpG by A52,ZFMISC_1:87;
hence thesis by A52,A55,NECKLACE:def 5;
end;
suppose
x = 2 & y = 3;
hence thesis by ENUMSET1:def 4,NECKLA_2:2;
end;
suppose
x = 3 & y = 0;
then [h.3,h.0] in (the InternalRel of G) /\ the InternalRel of CmpG
by A29,A52,XBOOLE_0:def 4;
then the InternalRel of G meets the InternalRel of CmpG;
hence thesis by Th12;
end;
suppose
x = 3 & y = 1;
then [h.3,h.1] in (the InternalRel of G) /\ the InternalRel of CmpG
by A27,A52,XBOOLE_0:def 4;
then the InternalRel of G meets the InternalRel of CmpG;
hence thesis by Th12;
end;
suppose
x = 3 & y = 2;
hence thesis by ENUMSET1:def 4,NECKLA_2:2;
end;
suppose
A56: x = 3 & y = 3;
then h.3 in the carrier of CmpG by A52,ZFMISC_1:87;
hence thesis by A52,A56,NECKLACE:def 5;
end;
end;
hence thesis by A4,A1,A6,A8;
end;
assume CmpG embeds N4;
then consider f being Function of N4, CmpG such that
A57: f is one-to-one and
A58: for x,y being Element of N4 holds [x,y] in the InternalRel of N4
iff [f.x,f.y] in the InternalRel of CmpG;
consider g being Function of N4,CmpN4 such that
A59: g is isomorphic by NECKLACE:29,WAYBEL_1:def 8;
A60: 2 in the carrier of N4 by A2,ENUMSET1:def 2;
A61: dom f = the carrier of N4 by FUNCT_2:def 1;
A62: [f.0,f.2] in the InternalRel of G
proof
assume
A63: not thesis;
[f.0,f.2] in the InternalRel of CmpG
proof
f.0 in the carrier of CmpG & f.2 in the carrier of CmpG by A3,A60,
FUNCT_2:5;
then [f.0,f.2] in [:the carrier of G,the carrier of G:] by A1,ZFMISC_1:87
;
then [f.0,f.2] in id (the carrier of G) \/ (the InternalRel of G) \/ (
the InternalRel of CmpG) by Th14;
then
A64: [f.0,f.2] in id (the carrier of G) \/ (the InternalRel of G) or [f
.0,f.2] in the InternalRel of CmpG by XBOOLE_0:def 3;
assume not thesis;
then [f.0,f.2] in id (the carrier of G) by A63,A64,XBOOLE_0:def 3;
then f.0 = f.2 by RELAT_1:def 10;
hence contradiction by A57,A61,A3,A60,FUNCT_1:def 4;
end;
then
A65: [0,2] in the InternalRel of N4 by A58,A3,A60;
[0,2] in the InternalRel of CmpN4 by Th11,ENUMSET1:def 4;
then [0,2] in (the InternalRel of N4) /\ (the InternalRel of CmpN4) by A65,
XBOOLE_0:def 4;
then the InternalRel of N4 meets the InternalRel of CmpN4;
hence thesis by Th12;
end;
A66: 3 in the carrier of N4 by A2,ENUMSET1:def 2;
A67: [f.0,f.3] in the InternalRel of G
proof
assume
A68: not [f.0,f.3] in the InternalRel of G;
[f.0,f.3] in the InternalRel of CmpG
proof
f.0 in the carrier of CmpG & f.3 in the carrier of CmpG by A3,A66,
FUNCT_2:5;
then [f.0,f.3] in [:the carrier of G,the carrier of G:] by A1,ZFMISC_1:87
;
then [f.0,f.3] in id (the carrier of G) \/ (the InternalRel of G) \/ (
the InternalRel of CmpG) by Th14;
then
A69: [f.0,f.3] in id (the carrier of G) \/ (the InternalRel of G) or [f
.0,f.3] in the InternalRel of CmpG by XBOOLE_0:def 3;
assume not thesis;
then [f.0,f.3] in id (the carrier of G) by A68,A69,XBOOLE_0:def 3;
then f.0 = f.3 by RELAT_1:def 10;
hence contradiction by A57,A61,A3,A66,FUNCT_1:def 4;
end;
then
A70: [0,3] in the InternalRel of N4 by A58,A3,A66;
[0,3] in the InternalRel of CmpN4 by Th11,ENUMSET1:def 4;
then [0,3] in (the InternalRel of N4) /\ (the InternalRel of CmpN4) by A70,
XBOOLE_0:def 4;
then the InternalRel of N4 meets the InternalRel of CmpN4;
hence thesis by Th12;
end;
A71: 1 in the carrier of N4 by A2,ENUMSET1:def 2;
A72: [f.1,f.3] in the InternalRel of G
proof
assume
A73: not [f.1,f.3] in the InternalRel of G;
[f.1,f.3] in the InternalRel of CmpG
proof
f.1 in the carrier of CmpG & f.3 in the carrier of CmpG by A71,A66,
FUNCT_2:5;
then [f.1,f.3] in [:the carrier of G,the carrier of G:] by A1,ZFMISC_1:87
;
then [f.1,f.3] in id (the carrier of G) \/ (the InternalRel of G) \/ (
the InternalRel of CmpG) by Th14;
then
A74: [f.1,f.3] in id (the carrier of G) \/ (the InternalRel of G) or [f
.1,f.3] in the InternalRel of CmpG by XBOOLE_0:def 3;
assume not thesis;
then [f.1,f.3] in id (the carrier of G) by A73,A74,XBOOLE_0:def 3;
then f.1 = f.3 by RELAT_1:def 10;
hence contradiction by A57,A61,A71,A66,FUNCT_1:def 4;
end;
then
A75: [1,3] in the InternalRel of N4 by A58,A71,A66;
[1,3] in the InternalRel of CmpN4 by Th11,ENUMSET1:def 4;
then [1,3] in (the InternalRel of N4) /\ (the InternalRel of CmpN4) by A75,
XBOOLE_0:def 4;
then the InternalRel of N4 meets the InternalRel of CmpN4;
hence thesis by Th12;
end;
[3,2] in the InternalRel of N4 by ENUMSET1:def 4,NECKLA_2:2;
then
A76: [f.3,f.2] in the InternalRel of CmpG by A58,A60,A66;
[2,3] in the InternalRel of N4 by ENUMSET1:def 4,NECKLA_2:2;
then
A77: [f.2,f.3] in the InternalRel of CmpG by A58,A60,A66;
[1,2] in the InternalRel of N4 by ENUMSET1:def 4,NECKLA_2:2;
then
A78: [f.1,f.2] in the InternalRel of CmpG by A58,A71,A60;
[1,0] in the InternalRel of N4 by ENUMSET1:def 4,NECKLA_2:2;
then
A79: [f.1,f.0] in the InternalRel of CmpG by A58,A3,A71;
A80: [f.2,f.0] in the InternalRel of G
proof
assume
A81: not [f.2,f.0] in the InternalRel of G;
[f.2,f.0] in the InternalRel of CmpG
proof
f.0 in the carrier of CmpG & f.2 in the carrier of CmpG by A3,A60,
FUNCT_2:5;
then [f.2,f.0] in [:the carrier of G,the carrier of G:] by A1,ZFMISC_1:87
;
then [f.2,f.0] in id (the carrier of G) \/ (the InternalRel of G) \/ (
the InternalRel of CmpG) by Th14;
then
A82: [f.2,f.0] in id (the carrier of G) \/ (the InternalRel of G) or [f
.2,f.0] in the InternalRel of CmpG by XBOOLE_0:def 3;
assume not thesis;
then [f.2,f.0] in id (the carrier of G) by A81,A82,XBOOLE_0:def 3;
then f.0 = f.2 by RELAT_1:def 10;
hence contradiction by A57,A61,A3,A60,FUNCT_1:def 4;
end;
then
A83: [2,0] in the InternalRel of N4 by A58,A3,A60;
[2,0] in the InternalRel of CmpN4 by Th11,ENUMSET1:def 4;
then [2,0] in (the InternalRel of N4) /\ (the InternalRel of CmpN4) by A83,
XBOOLE_0:def 4;
then the InternalRel of N4 meets the InternalRel of CmpN4;
hence thesis by Th12;
end;
A84: [f.3,f.0] in the InternalRel of G
proof
assume
A85: not [f.3,f.0] in the InternalRel of G;
[f.3,f.0] in the InternalRel of CmpG
proof
f.0 in the carrier of CmpG & f.3 in the carrier of CmpG by A3,A66,
FUNCT_2:5;
then [f.3,f.0] in [:the carrier of G,the carrier of G:] by A1,ZFMISC_1:87
;
then [f.3,f.0] in id (the carrier of G) \/ (the InternalRel of G) \/ (
the InternalRel of CmpG) by Th14;
then
A86: [f.3,f.0] in id (the carrier of G) \/ (the InternalRel of G) or [f
.3,f.0] in the InternalRel of CmpG by XBOOLE_0:def 3;
assume not thesis;
then [f.3,f.0] in id (the carrier of G) by A85,A86,XBOOLE_0:def 3;
then f.0 = f.3 by RELAT_1:def 10;
hence contradiction by A57,A61,A3,A66,FUNCT_1:def 4;
end;
then
A87: [3,0] in the InternalRel of N4 by A58,A3,A66;
[3,0] in the InternalRel of CmpN4 by Th11,ENUMSET1:def 4;
then [3,0] in (the InternalRel of N4) /\ (the InternalRel of CmpN4) by A87,
XBOOLE_0:def 4;
then the InternalRel of N4 meets the InternalRel of CmpN4;
hence thesis by Th12;
end;
A88: [f.3,f.1] in the InternalRel of G
proof
assume
A89: not [f.3,f.1] in the InternalRel of G;
[f.3,f.1] in the InternalRel of CmpG
proof
f.1 in the carrier of CmpG & f.3 in the carrier of CmpG by A71,A66,
FUNCT_2:5;
then [f.3,f.1] in [:the carrier of G,the carrier of G:] by A1,ZFMISC_1:87
;
then [f.3,f.1] in id (the carrier of G) \/ (the InternalRel of G) \/ (
the InternalRel of CmpG) by Th14;
then
A90: [f.3,f.1] in id (the carrier of G) \/ (the InternalRel of G) or [f
.3,f.1] in the InternalRel of CmpG by XBOOLE_0:def 3;
assume not thesis;
then [f.3,f.1] in id (the carrier of G) by A89,A90,XBOOLE_0:def 3;
then f.1 = f.3 by RELAT_1:def 10;
hence contradiction by A57,A61,A71,A66,FUNCT_1:def 4;
end;
then
A91: [3,1] in the InternalRel of N4 by A58,A71,A66;
[3,1] in the InternalRel of CmpN4 by Th11,ENUMSET1:def 4;
then [3,1] in (the InternalRel of N4) /\ (the InternalRel of CmpN4) by A91,
XBOOLE_0:def 4;
then the InternalRel of N4 meets the InternalRel of CmpN4;
hence thesis by Th12;
end;
[2,1] in the InternalRel of N4 by ENUMSET1:def 4,NECKLA_2:2;
then
A92: [f.2,f.1] in the InternalRel of CmpG by A58,A71,A60;
[0,1] in the InternalRel of N4 by ENUMSET1:def 4,NECKLA_2:2;
then
A93: [f.0,f.1] in the InternalRel of CmpG by A58,A3,A71;
A94: for x,y being Element of CmpN4 holds [x,y] in the InternalRel of CmpN4
iff [f.x,f.y] in the InternalRel of G
proof
let x,y be Element of CmpN4;
A95: the carrier of N4 = the carrier of CmpN4 by NECKLACE:def 8;
thus [x,y] in the InternalRel of CmpN4 implies [f.x,f.y] in the
InternalRel of G
proof
assume
A96: [x,y] in the InternalRel of CmpN4;
per cases by A96,Th11,ENUMSET1:def 4;
suppose
A97: [x,y] = [0,2];
then x = 0 by XTUPLE_0:1;
hence thesis by A62,A97,XTUPLE_0:1;
end;
suppose
A98: [x,y] = [2,0];
then x = 2 by XTUPLE_0:1;
hence thesis by A80,A98,XTUPLE_0:1;
end;
suppose
A99: [x,y] = [0,3];
then x = 0 by XTUPLE_0:1;
hence thesis by A67,A99,XTUPLE_0:1;
end;
suppose
A100: [x,y] = [3,0];
then x = 3 by XTUPLE_0:1;
hence thesis by A84,A100,XTUPLE_0:1;
end;
suppose
A101: [x,y] = [1,3];
then x = 1 by XTUPLE_0:1;
hence thesis by A72,A101,XTUPLE_0:1;
end;
suppose
A102: [x,y] = [3,1];
then x = 3 by XTUPLE_0:1;
hence thesis by A88,A102,XTUPLE_0:1;
end;
end;
assume
A103: [f.x,f.y] in the InternalRel of G;
per cases by A2,A95,ENUMSET1:def 2;
suppose
A104: x = 0 & y = 0;
then f.0 in the carrier of G by A103,ZFMISC_1:87;
hence thesis by A103,A104,NECKLACE:def 5;
end;
suppose
x = 0 & y = 1;
then [f.0,f.1] in (the InternalRel of G) /\ the InternalRel of CmpG by
A93,A103,XBOOLE_0:def 4;
then the InternalRel of G meets the InternalRel of CmpG;
hence thesis by Th12;
end;
suppose
x = 0 & y = 2;
hence thesis by Th11,ENUMSET1:def 4;
end;
suppose
x = 0 & y = 3;
hence thesis by Th11,ENUMSET1:def 4;
end;
suppose
x = 1 & y = 0;
then [f.1,f.0] in (the InternalRel of G) /\ the InternalRel of CmpG by
A79,A103,XBOOLE_0:def 4;
then the InternalRel of G meets the InternalRel of CmpG;
hence thesis by Th12;
end;
suppose
x = 2 & y = 0;
hence thesis by Th11,ENUMSET1:def 4;
end;
suppose
x = 3 & y = 0;
hence thesis by Th11,ENUMSET1:def 4;
end;
suppose
A105: x = 1 & y = 1;
then f.1 in the carrier of G by A103,ZFMISC_1:87;
hence thesis by A103,A105,NECKLACE:def 5;
end;
suppose
x = 1 & y = 2;
then [f.1,f.2] in (the InternalRel of G) /\ the InternalRel of CmpG by
A78,A103,XBOOLE_0:def 4;
then the InternalRel of G meets the InternalRel of CmpG;
hence thesis by Th12;
end;
suppose
x = 1 & y = 3;
hence thesis by Th11,ENUMSET1:def 4;
end;
suppose
x = 2 & y = 1;
then [f.2,f.1] in (the InternalRel of G) /\ the InternalRel of CmpG by
A92,A103,XBOOLE_0:def 4;
then the InternalRel of G meets the InternalRel of CmpG;
hence thesis by Th12;
end;
suppose
A106: x = 2 & y = 2;
then f.2 in the carrier of G by A103,ZFMISC_1:87;
hence thesis by A103,A106,NECKLACE:def 5;
end;
suppose
x = 2 & y = 3;
then [f.2,f.3] in (the InternalRel of G) /\ the InternalRel of CmpG by
A77,A103,XBOOLE_0:def 4;
then the InternalRel of G meets the InternalRel of CmpG;
hence thesis by Th12;
end;
suppose
x = 3 & y = 1;
hence thesis by Th11,ENUMSET1:def 4;
end;
suppose
x = 3 & y = 2;
then [f.3,f.2] in (the InternalRel of G) /\ the InternalRel of CmpG by
A76,A103,XBOOLE_0:def 4;
then the InternalRel of G meets the InternalRel of CmpG;
hence thesis by Th12;
end;
suppose
A107: x = 3 & y = 3;
then f.3 in the carrier of G by A103,ZFMISC_1:87;
hence thesis by A103,A107,NECKLACE:def 5;
end;
end;
reconsider f as Function of CmpN4,G by A4,NECKLACE:def 8;
reconsider h = f*g as Function of N4,G;
A108: g is one-to-one monotone by A59,WAYBEL_0:def 38;
for x,y being Element of N4 holds [x,y] in the InternalRel of N4 iff [
h.x,h.y] in the InternalRel of G
proof
let x,y be Element of N4;
thus [x,y] in the InternalRel of N4 implies [h.x,h.y] in the InternalRel
of G
proof
assume [x,y] in the InternalRel of N4;
then x <= y by ORDERS_2:def 5;
then g.x <= g.y by A108,WAYBEL_1:def 2;
then [g.x,g.y] in the InternalRel of CmpN4 by ORDERS_2:def 5;
then [f.(g.x),f.(g.y)] in the InternalRel of G by A94;
then [(f*g).x,f.(g.y)] in the InternalRel of G by FUNCT_2:15;
hence thesis by FUNCT_2:15;
end;
assume [h.x,h.y] in the InternalRel of G;
then [f.(g.x),h.y] in the InternalRel of G by FUNCT_2:15;
then [f.(g.x),f.(g.y)] in the InternalRel of G by FUNCT_2:15;
then [g.x,g.y] in the InternalRel of CmpN4 by A94;
then g.x <= g.y by ORDERS_2:def 5;
then x <= y by A59,WAYBEL_0:66;
hence thesis by ORDERS_2:def 5;
end;
hence thesis by A57,A108;
end;
theorem Th25:
for G being non empty irreflexive RelStr holds G is N-free iff
ComplRelStr G is N-free
proof
let G be non empty irreflexive RelStr;
thus G is N-free implies ComplRelStr G is N-free
proof
assume
A1: G is N-free;
assume not thesis;
then ComplRelStr G embeds Necklace 4 by NECKLA_2:def 1;
then G embeds Necklace 4 by Th24;
hence contradiction by A1,NECKLA_2:def 1;
end;
assume
A2: ComplRelStr G is N-free;
assume not thesis;
then G embeds Necklace 4 by NECKLA_2:def 1;
then ComplRelStr G embeds Necklace 4 by Th24;
hence contradiction by A2,NECKLA_2:def 1;
end;
begin :: Connected Graphs
definition
let R be RelStr;
mode path of R is RedSequence of the InternalRel of R;
end;
definition
let R be RelStr;
attr R is path-connected means
for x,y being set st x in the carrier
of R & y in the carrier of R & x <> y holds the InternalRel of R reduces x,y or
the InternalRel of R reduces y,x;
end;
registration
cluster empty -> path-connected for RelStr;
correctness;
end;
registration
cluster connected -> path-connected for non empty RelStr;
correctness
proof
let R be non empty RelStr;
set cR = the carrier of R, IR = the InternalRel of R;
assume
A1: R is connected;
for x,y being set st x in the carrier of R & y in the carrier of R & x
<> y holds (the InternalRel of R) reduces x,y or (the InternalRel of R) reduces
y,x
proof
let x,y being set such that
A2: x in cR & y in cR and
x <> y;
reconsider x,y as Element of R by A2;
A3: x <= y or y <= x by A1,WAYBEL_0:def 29;
per cases by A3,ORDERS_2:def 5;
suppose
A4: [x,y] in IR;
A5: len <*x,y*> = 2 & <*x,y*>.1 = x by FINSEQ_1:44;
A6: <*x,y*>.2 = y;
<*x,y*> is RedSequence of IR by A4,REWRITE1:7;
hence thesis by A5,A6,REWRITE1:def 3;
end;
suppose
A7: [y,x] in IR;
A8: len <*y,x*> = 2 & <*y,x*>.1 = y by FINSEQ_1:44;
A9: <*y,x*>.2 = x;
<*y,x*> is RedSequence of IR by A7,REWRITE1:7;
hence thesis by A8,A9,REWRITE1:def 3;
end;
end;
hence thesis;
end;
end;
theorem Th26:
for R being non empty transitive reflexive RelStr, x,y being
Element of R holds the InternalRel of R reduces x,y implies [x,y] in the
InternalRel of R
proof
let R be non empty transitive reflexive RelStr;
let x,y be Element of R;
set cR = the carrier of R, IR = the InternalRel of R;
assume IR reduces x,y;
then consider p being RedSequence of IR such that
A1: p.1 = x and
A2: p.len p = y by REWRITE1:def 3;
reconsider p as FinSequence;
defpred P[Nat] means $1 in dom p implies [p.1,p.$1] in IR;
A3: IR is_transitive_in cR by ORDERS_2:def 3;
A4: for k be non zero Nat st P[k] holds P[k+1]
proof
let k be non zero Nat such that
A5: P[k];
assume
A6: k+1 in dom p;
then k <= k+1 & k+1 <= len p by FINSEQ_3:25,NAT_1:11;
then
A7: 0 + 1 <= k & k <= len p by NAT_1:13;
then
A8: p.1 in cR by A5,FINSEQ_3:25,ZFMISC_1:87;
k in dom p by A7,FINSEQ_3:25;
then
A9: [p.k,p.(k+1)] in IR by A6,REWRITE1:def 2;
then p.k in cR & p.(k+1) in cR by ZFMISC_1:87;
hence thesis by A3,A5,A7,A9,A8,FINSEQ_3:25;
end;
IR is_reflexive_in cR by ORDERS_2:def 2;
then
A10: P[1] by A1;
A11: for k be non zero Nat holds P[k] from NAT_1:sch 10(A10,A4);
A12: len p > 0 by REWRITE1:def 2;
then 0 + 1 <= len p by NAT_1:13;
then len p in dom p by FINSEQ_3:25;
hence thesis by A1,A2,A12,A11;
end;
registration
cluster path-connected -> connected for
non empty transitive reflexive RelStr;
correctness
proof
let R be non empty transitive reflexive RelStr;
set IR = the InternalRel of R;
assume
A1: R is path-connected;
for x,y being Element of R holds x <= y or y <= x
proof
let x,y being Element of R;
per cases;
suppose
x = y;
hence thesis;
end;
suppose
x <> y;
then IR reduces x,y or IR reduces y,x by A1;
then [x,y] in IR or [y,x] in IR by Th26;
hence thesis by ORDERS_2:def 5;
end;
end;
hence thesis by WAYBEL_0:def 29;
end;
end;
theorem Th27:
for R be symmetric RelStr,x,y being set holds the InternalRel of
R reduces x,y implies the InternalRel of R reduces y,x
proof
let R be symmetric RelStr;
set IR = the InternalRel of R;
let x,y be set;
A1: IR = IR~ by RELAT_2:13;
assume IR reduces x,y;
then consider p being RedSequence of IR such that
A2: p.1 = x and
A3: p.len p = y by REWRITE1:def 3;
reconsider p as FinSequence;
A4: (Rev p).len p = x by A2,FINSEQ_5:62;
IR reduces y,x
proof
reconsider q = Rev p as RedSequence of IR by A1,REWRITE1:9;
q.1 = y & q.len q = x by A3,A4,FINSEQ_5:62,def 3;
hence thesis by REWRITE1:def 3;
end;
hence thesis;
end;
definition
let R be symmetric RelStr;
redefine attr R is path-connected means :: redefines path-connected (NECKLA_3, definition)
for x,y being set st x in the
carrier of R & y in the carrier of R & x <> y holds (the InternalRel of R)
reduces x,y;
compatibility
proof
set IR = the InternalRel of R, cR = the carrier of R;
thus R is path-connected implies for x,y being set st x in the carrier of
R & y in the carrier of R & x <> y holds (the InternalRel of R) reduces x,y
proof
assume
A1: R is path-connected;
let x,y being set such that
A2: x in cR & y in cR & x <> y;
per cases by A1,A2;
suppose
IR reduces x,y;
hence thesis;
end;
suppose
IR reduces y,x;
hence thesis by Th27;
end;
end;
assume for x,y be set st x in the carrier of R & y in the carrier of R &
x <> y holds IR reduces x,y;
then
for x,y being set st x in the carrier of R & y in the carrier of R & x
<> y holds (the InternalRel of R) reduces x,y or (the InternalRel of R) reduces
y,x;
hence thesis;
end;
end;
definition
let R be RelStr;
let x be Element of R;
func component x -> Subset of R equals
Class(EqCl the InternalRel of R, x);
coherence;
end;
registration
let R be non empty RelStr;
let x be Element of R;
cluster component x -> non empty;
correctness by EQREL_1:20;
end;
theorem Th28:
for R being RelStr, x being Element of R, y be set st y in
component x holds [x,y] in EqCl the InternalRel of R
proof
let R be RelStr;
let x be Element of R;
let y be set;
set IR = the InternalRel of R;
assume y in component x;
then [y,x] in EqCl IR by EQREL_1:19;
hence thesis by EQREL_1:6;
end;
theorem Th29:
for R being RelStr, x being Element of R, A being set holds A =
component x iff
for y being object holds y in A iff [x,y] in EqCl the InternalRel of R
proof
let R be RelStr;
let x being Element of R;
let A be set;
set IR = the InternalRel of R;
A1: (for y being object
holds y in A iff [x,y] in EqCl (the InternalRel of R))
implies A = component x
proof
assume
A2: for y being object holds y in A iff [x,y] in EqCl (the InternalRel of R);
A3: component x c= A
proof
let a be object;
assume a in component x;
then [a,x] in EqCl IR by EQREL_1:19;
then [x,a] in EqCl IR by EQREL_1:6;
hence thesis by A2;
end;
A c= component x
proof
let a be object;
assume a in A;
then [x,a] in EqCl IR by A2;
then [a,x] in EqCl IR by EQREL_1:6;
hence thesis by EQREL_1:19;
end;
hence thesis by A3;
end;
A = component x implies
for y being object holds [x,y] in EqCl IR implies y in A
proof
assume
A4: A = component x;
let y be object;
assume [x,y] in EqCl IR;
then [y,x] in EqCl IR by EQREL_1:6;
hence thesis by A4,EQREL_1:19;
end;
hence thesis by A1,Th28;
end;
theorem Th30:
for R be non empty irreflexive symmetric RelStr holds R is not
path-connected implies ex G1,G2 being non empty strict irreflexive symmetric
RelStr st the carrier of G1 misses the carrier of G2 & the RelStr of R =
union_of(G1,G2)
proof
let R be non empty irreflexive symmetric RelStr;
set cR = the carrier of R, IR = the InternalRel of R;
assume R is not path-connected;
then consider x,y being set such that
A1: x in cR & y in cR and
x <> y and
A2: not IR reduces x,y;
reconsider x,y as Element of R by A1;
set A1 = component x, A2 = (the carrier of R) \ A1;
reconsider A2 as Subset of R;
set G1 = subrelstr A1, G2 = subrelstr A2;
A3: the carrier of G2 = A2 by YELLOW_0:def 15;
cR c= A1 \/ A2
proof
let a be object;
assume
A4: a in cR;
assume not thesis;
then ( not a in A1)& not a in A2 by XBOOLE_0:def 3;
hence contradiction by A4,XBOOLE_0:def 5;
end;
then
A5: cR = A1 \/ A2;
A6: the carrier of G1 = A1 by YELLOW_0:def 15;
then
A7: (the carrier of G1) misses (the carrier of G2) by A3,XBOOLE_1:79;
A8: the InternalRel of G1 misses the InternalRel of G2
proof
set IG1 = the InternalRel of G1, IG2 = the InternalRel of G2;
assume not thesis;
then IG1 /\ IG2 <> {};
then consider a be object such that
A9: a in IG1 /\ IG2 by XBOOLE_0:def 1;
a in IG1 by A9,XBOOLE_0:def 4;
then consider c1,c2 be object such that
A10: a = [c1,c2] and
A11: c1 in A1 and
c2 in A1 by A6,RELSET_1:2;
ex g1,g2 be object st a = [g1,g2] & g1 in A2 & g2 in A2
by A3,A9,RELSET_1:2;
then c1 in A2 by A10,XTUPLE_0:1;
then c1 in A1 /\ A2 by A11,XBOOLE_0:def 4;
hence contradiction by A6,A3,A7;
end;
A12: the InternalRel of G2 = IR \ (the InternalRel of G1)
proof
set IG1 = the InternalRel of G1, IG2 = the InternalRel of G2;
thus IG2 c= IR \ IG1
proof
let a be object;
assume
A13: a in IG2;
then consider g1,g2 be object such that
A14: a = [g1,g2] and
A15: g1 in A2 & g2 in A2 by A3,RELSET_1:2;
reconsider g1,g2 as Element of G2 by A15,YELLOW_0:def 15;
reconsider u1 = g1, u2 = g2 as Element of R by A15;
A16: not a in IG1
by A13,XBOOLE_0:def 4,A8;
g1 <= g2 by A13,A14,ORDERS_2:def 5;
then u1 <= u2 by YELLOW_0:59;
then a in IR by A14,ORDERS_2:def 5;
hence thesis by A16,XBOOLE_0:def 5;
end;
let a be object;
assume
A17: a in IR \ IG1;
then
A18: a in IR by XBOOLE_0:def 5;
A19: not a in IG1 by A17,XBOOLE_0:def 5;
consider c1,c2 be object such that
A20: a = [c1,c2] and
A21: c1 in cR & c2 in cR by A17,RELSET_1:2;
reconsider c1,c2 as Element of R by A21;
A22: c1 <= c2 by A18,A20,ORDERS_2:def 5;
per cases by A5,XBOOLE_0:def 3;
suppose
A23: c1 in A1 & c2 in A1;
then reconsider d2 = c2 as Element of G1 by YELLOW_0:def 15;
reconsider d1 = c1 as Element of G1 by A23,YELLOW_0:def 15;
d1 <= d2 by A6,A22,YELLOW_0:60;
hence thesis by A19,A20,ORDERS_2:def 5;
end;
suppose
A24: c1 in A1 & c2 in A2;
A25: [:A1,A2:] misses IR
proof
assume not thesis;
then [:A1,A2:] /\ IR <> {};
then consider b be object such that
A26: b in [:A1,A2:] /\ IR by XBOOLE_0:def 1;
A27: b in IR by A26,XBOOLE_0:def 4;
b in [:A1,A2:] by A26,XBOOLE_0:def 4;
then consider b1,b2 be object such that
A28: b1 in A1 and
A29: b2 in A2 and
A30: b = [b1,b2] by ZFMISC_1:def 2;
reconsider b2 as Element of R by A29;
reconsider b1 as Element of R by A28;
IR c= EqCl IR & [x,b1] in EqCl IR by A28,Th29,MSUALG_5:def 1;
then [x,b2] in EqCl IR by A27,A30,EQREL_1:7;
then b2 in A1 by Th29;
then b2 in A1 /\ A2 by A29,XBOOLE_0:def 4;
hence thesis by A6,A3,A7;
end;
a in [:A1,A2:] by A20,A24,ZFMISC_1:def 2;
then a in [:A1,A2:] /\ IR by A18,XBOOLE_0:def 4;
hence thesis by A25;
end;
suppose
A31: c1 in A2 & c2 in A1;
A32: [:A2,A1:] misses IR
proof
assume not thesis;
then [:A2,A1:] /\ IR <> {};
then consider b be object such that
A33: b in [:A2,A1:] /\ IR by XBOOLE_0:def 1;
b in [:A2,A1:] by A33,XBOOLE_0:def 4;
then consider b1,b2 be object such that
A34: b1 in A2 and
A35: b2 in A1 and
A36: b = [b1,b2] by ZFMISC_1:def 2;
reconsider b1 as Element of R by A34;
reconsider b2 as Element of R by A35;
A37: [x,b2] in EqCl IR by A35,Th29;
A38: IR c= EqCl IR by MSUALG_5:def 1;
b in IR by A33,XBOOLE_0:def 4;
then [b2,b1] in EqCl IR by A36,A38,EQREL_1:6;
then [x,b1] in EqCl IR by A37,EQREL_1:7;
then b1 in A1 by Th29;
then b1 in A1 /\ A2 by A34,XBOOLE_0:def 4;
hence thesis by A6,A3,A7;
end;
a in [:A2,A1:] by A20,A31,ZFMISC_1:def 2;
then a in [:A2,A1:] /\ IR by A18,XBOOLE_0:def 4;
hence thesis by A32;
end;
suppose
A39: c1 in A2 & c2 in A2;
then reconsider d2 = c2 as Element of G2 by YELLOW_0:def 15;
reconsider d1 = c1 as Element of G2 by A39,YELLOW_0:def 15;
d1 <= d2 by A3,A22,A39,YELLOW_0:60;
hence thesis by A20,ORDERS_2:def 5;
end;
end;
IR = (the InternalRel of G1) \/ (the InternalRel of G2)
proof
set IG1 = the InternalRel of G1, IG2 = the InternalRel of G2;
thus IR c= IG1 \/ IG2
proof
let a be object;
assume
A40: a in IR;
assume not thesis;
then ( not a in IG1)& not a in IG2 by XBOOLE_0:def 3;
hence contradiction by A12,A40,XBOOLE_0:def 5;
end;
let a be object;
assume
A41: a in IG1 \/ IG2;
per cases by A41,XBOOLE_0:def 3;
suppose
A42: a in IG1;
then consider v,w be object such that
A43: a = [v,w] and
A44: v in A1 & w in A1 by A6,RELSET_1:2;
reconsider v,w as Element of G1 by A44,YELLOW_0:def 15;
reconsider u1 = v, u2 = w as Element of R by A44;
v <= w by A42,A43,ORDERS_2:def 5;
then u1 <= u2 by YELLOW_0:59;
hence thesis by A43,ORDERS_2:def 5;
end;
suppose
A45: a in IG2;
then consider v,w be object such that
A46: a = [v,w] and
A47: v in A2 & w in A2 by A3,RELSET_1:2;
reconsider v,w as Element of G2 by A47,YELLOW_0:def 15;
reconsider u1 = v, u2 = w as Element of R by A47;
v <= w by A45,A46,ORDERS_2:def 5;
then u1 <= u2 by YELLOW_0:59;
hence thesis by A46,ORDERS_2:def 5;
end;
end;
then
A48: IR = the InternalRel of union_of(G1,G2) by NECKLA_2:def 2;
IR = IR~ by RELAT_2:13;
then not IR \/ IR~ reduces x,y by A2;
then not x,y are_convertible_wrt IR by REWRITE1:def 4;
then not [x,y] in EqCl IR by MSUALG_6:41;
then not y in A1 by Th29;
then
A49: G2 is non empty strict RelStr by A3,XBOOLE_0:def 5;
cR = the carrier of union_of(G1,G2) by A6,A3,A5,NECKLA_2:def 2;
hence thesis by A6,A7,A49,A48;
end;
theorem Th31:
for R be non empty irreflexive symmetric RelStr holds
ComplRelStr R is not path-connected implies ex G1,G2 being non empty strict
irreflexive symmetric RelStr st the carrier of G1 misses the carrier of G2 &
the RelStr of R = sum_of(G1,G2)
proof
let R be non empty irreflexive symmetric RelStr;
set cR = the carrier of R, IR = the InternalRel of R, CR = ComplRelStr R,
ICR = the InternalRel of ComplRelStr R, cCR = the carrier of ComplRelStr R;
assume CR is not path-connected;
then consider x,y being set such that
A1: x in cCR and
A2: y in cCR and
x <> y and
A3: not ICR reduces x,y;
reconsider x,y as Element of CR by A1,A2;
set A1 = component x, A2 = (the carrier of R) \ A1;
reconsider A1 as Subset of R by NECKLACE:def 8;
ICR = ICR~ by RELAT_2:13;
then not ICR \/ ICR~ reduces x,y by A3;
then not x,y are_convertible_wrt ICR by REWRITE1:def 4;
then not [x,y] in EqCl ICR by MSUALG_6:41;
then
A4: not y in A1 by Th29;
reconsider A2 as Subset of R;
set G1 = subrelstr A1, G2 = subrelstr A2;
A5: the carrier of G1 = A1 by YELLOW_0:def 15;
set IG1 = the InternalRel of G1, IG2 = the InternalRel of G2, G1G2 = [:the
carrier of G1,the carrier of G2:], G2G1 = [:the carrier of G2,the carrier of G1
:];
A6: cR = A1 \/ A2
proof
thus cR c= A1 \/ A2
proof
let a be object;
assume
A7: a in cR;
assume not thesis;
then ( not a in A1)& not a in A2 by XBOOLE_0:def 3;
hence contradiction by A7,XBOOLE_0:def 5;
end;
let a be object;
assume
A8: a in A1 \/ A2;
per cases by A8,XBOOLE_0:def 3;
suppose
a in A1;
hence thesis;
end;
suppose
a in A2;
hence thesis;
end;
end;
A9: the carrier of G2 = A2 by YELLOW_0:def 15;
then
A10: (the carrier of G1) misses (the carrier of G2) by A5,XBOOLE_1:79;
A11: the InternalRel of G1 misses the InternalRel of G2
proof
assume not thesis;
then IG1 /\ IG2 <> {};
then consider a be object such that
A12: a in IG1 /\ IG2 by XBOOLE_0:def 1;
a in IG1 by A12,XBOOLE_0:def 4;
then consider c1,c2 be object such that
A13: a = [c1,c2] and
A14: c1 in A1 and
c2 in A1 by A5,RELSET_1:2;
ex g1,g2 be object st a = [g1,g2] & g1 in A2 & g2 in A2
by A9,A12,RELSET_1:2;
then c1 in A2 by A13,XTUPLE_0:1;
then c1 in A1 /\ A2 by A14,XBOOLE_0:def 4;
hence contradiction by A5,A9,A10;
end;
A15: the InternalRel of G2 = IR \ IG1 \ G1G2 \ G2G1
proof
thus IG2 c= IR \ IG1 \ G1G2 \ G2G1
proof
let a be object;
assume
A16: a in IG2;
then consider g1,g2 be object such that
A17: a = [g1,g2] and
A18: g1 in A2 and
A19: g2 in A2 by A9,RELSET_1:2;
reconsider g1,g2 as Element of G2 by A18,A19,YELLOW_0:def 15;
reconsider u1 = g1, u2 = g2 as Element of R by A18,A19;
A20: not a in IG1
by A16,XBOOLE_0:def 4,A11;
A21: not a in G2G1
proof
assume a in G2G1;
then g2 in A1 by A5,A17,ZFMISC_1:87;
then g2 in A1 /\ A2 by A19,XBOOLE_0:def 4;
hence thesis by A5,A9,A10;
end;
A22: not a in G1G2
proof
assume a in G1G2;
then g1 in A1 by A5,A17,ZFMISC_1:87;
then g1 in A1 /\ A2 by A18,XBOOLE_0:def 4;
hence thesis by A5,A9,A10;
end;
g1 <= g2 by A16,A17,ORDERS_2:def 5;
then u1 <= u2 by YELLOW_0:59;
then a in IR by A17,ORDERS_2:def 5;
then a in IR \ IG1 by A20,XBOOLE_0:def 5;
then a in IR \ IG1 \ G1G2 by A22,XBOOLE_0:def 5;
hence thesis by A21,XBOOLE_0:def 5;
end;
let a be object;
assume
A23: a in IR \ IG1 \ G1G2 \ G2G1;
then
A24: not a in G2G1 by XBOOLE_0:def 5;
A25: a in IR \ IG1 \ G1G2 by A23,XBOOLE_0:def 5;
then
A26: a in IR \ IG1 by XBOOLE_0:def 5;
then
A27: not a in IG1 by XBOOLE_0:def 5;
A28: not a in G1G2 by A25,XBOOLE_0:def 5;
consider c1,c2 be object such that
A29: a = [c1,c2] and
A30: c1 in cR & c2 in cR by A23,RELSET_1:2;
reconsider c1,c2 as Element of R by A30;
a in IR by A26,XBOOLE_0:def 5;
then
A31: c1 <= c2 by A29,ORDERS_2:def 5;
per cases by A6,XBOOLE_0:def 3;
suppose
A32: c1 in A1 & c2 in A1;
then reconsider d2 = c2 as Element of G1 by YELLOW_0:def 15;
reconsider d1 = c1 as Element of G1 by A32,YELLOW_0:def 15;
d1 <= d2 by A5,A31,YELLOW_0:60;
hence thesis by A27,A29,ORDERS_2:def 5;
end;
suppose
c1 in A1 & c2 in A2;
hence thesis by A5,A9,A28,A29,ZFMISC_1:87;
end;
suppose
c1 in A2 & c2 in A1;
hence thesis by A5,A9,A24,A29,ZFMISC_1:87;
end;
suppose
A33: c1 in A2 & c2 in A2;
then reconsider d1 = c1,d2 = c2 as Element of G2 by YELLOW_0:def 15;
d1 <= d2 by A9,A31,A33,YELLOW_0:60;
hence thesis by A29,ORDERS_2:def 5;
end;
end;
IR = (the InternalRel of G1) \/ (the InternalRel of G2) \/ [:the
carrier of G1,the carrier of G2:] \/ [:the carrier of G2,the carrier of G1:]
proof
set G1G2 = [:the carrier of G1,the carrier of G2:], G2G1 = [:the carrier
of G2,the carrier of G1:];
thus IR c= IG1 \/ IG2 \/ G1G2 \/ G2G1
proof
let a be object;
assume
A34: a in IR;
assume
A35: not thesis;
then
A36: not a in (IG1 \/ IG2 \/ G1G2) by XBOOLE_0:def 3;
then
A37: not a in (IG1 \/ IG2) by XBOOLE_0:def 3;
then not a in IG2 by XBOOLE_0:def 3;
then not a in IR \ IG1 \ G1G2 or a in G2G1 by A15,XBOOLE_0:def 5;
then
A38: not a in IR \ IG1 or a in G1G2 or a in G2G1 by XBOOLE_0:def 5;
not a in IG1 by A37,XBOOLE_0:def 3;
hence thesis by A34,A35,A36,A38,XBOOLE_0:def 3,def 5;
end;
let a be object;
assume a in IG1 \/ IG2 \/ G1G2 \/ G2G1;
then a in IG1 \/ IG2 \/ G1G2 or a in G2G1 by XBOOLE_0:def 3;
then
A39: a in IG1 \/ IG2 or a in G1G2 or a in G2G1 by XBOOLE_0:def 3;
per cases by A39,XBOOLE_0:def 3;
suppose
A40: a in IG1;
then consider v,w be object such that
A41: a = [v,w] and
A42: v in A1 & w in A1 by A5,RELSET_1:2;
reconsider v,w as Element of G1 by A42,YELLOW_0:def 15;
reconsider u1 = v, u2 = w as Element of R by A42;
v <= w by A40,A41,ORDERS_2:def 5;
then u1 <= u2 by YELLOW_0:59;
hence thesis by A41,ORDERS_2:def 5;
end;
suppose
A43: a in IG2;
then consider v,w be object such that
A44: a = [v,w] and
A45: v in A2 & w in A2 by A9,RELSET_1:2;
reconsider v,w as Element of G2 by A45,YELLOW_0:def 15;
reconsider u1 = v, u2 = w as Element of R by A45;
v <= w by A43,A44,ORDERS_2:def 5;
then u1 <= u2 by YELLOW_0:59;
hence thesis by A44,ORDERS_2:def 5;
end;
suppose
A46: a in G1G2;
assume
A47: not thesis;
consider v,w be object such that
A48: a = [v,w] by A46,RELAT_1:def 1;
A49: w in A2 by A9,A46,A48,ZFMISC_1:87;
A50: v in A1 by A5,A46,A48,ZFMISC_1:87;
then reconsider v,w as Element of CR by A49,NECKLACE:def 8;
v <> w
by A5,A9,A10,A50,A49,XBOOLE_0:def 4;
then
A51: not a in id cR by A48,RELAT_1:def 10;
[v,w] in [:cR,cR:] by A50,A49,ZFMISC_1:87;
then a in [:cR,cR:] \ IR by A48,A47,XBOOLE_0:def 5;
then a in IR` by SUBSET_1:def 4;
then a in IR` \ id cR by A51,XBOOLE_0:def 5;
then [v,w] in ICR by A48,NECKLACE:def 8;
then v,w are_convertible_wrt ICR by REWRITE1:29;
then
A52: [v,w] in EqCl ICR by MSUALG_6:41;
[x,v] in EqCl ICR by A50,Th29;
then [x,w] in EqCl ICR by A52,EQREL_1:7;
then w in component x by Th29;
then w in A1 /\ A2 by A49,XBOOLE_0:def 4;
hence thesis by A5,A9,A10;
end;
suppose
A53: a in G2G1;
assume
A54: not thesis;
consider v,w be object such that
A55: a = [v,w] by A53,RELAT_1:def 1;
A56: w in A1 by A5,A53,A55,ZFMISC_1:87;
A57: v in A2 by A9,A53,A55,ZFMISC_1:87;
then reconsider v,w as Element of CR by A56,NECKLACE:def 8;
v <> w
by A5,A9,A10,A57,A56,XBOOLE_0:def 4;
then
A58: not a in id cR by A55,RELAT_1:def 10;
[v,w] in [:cR,cR:] by A57,A56,ZFMISC_1:87;
then a in [:cR,cR:] \ IR by A55,A54,XBOOLE_0:def 5;
then a in IR` by SUBSET_1:def 4;
then a in IR` \ id cR by A58,XBOOLE_0:def 5;
then [v,w] in ICR by A55,NECKLACE:def 8;
then v,w are_convertible_wrt ICR by REWRITE1:29;
then [v,w] in EqCl ICR by MSUALG_6:41;
then
A59: [w,v] in EqCl ICR by EQREL_1:6;
[x,w] in EqCl ICR by A56,Th29;
then [x,v] in EqCl ICR by A59,EQREL_1:7;
then v in component x by Th29;
then v in A1 /\ A2 by A57,XBOOLE_0:def 4;
hence thesis by A5,A9,A10;
end;
end;
then
A60: IR = the InternalRel of sum_of(G1,G2) by NECKLA_2:def 3;
y in cR by A2,NECKLACE:def 8;
then
A61: G2 is non empty strict RelStr by A9,A4,XBOOLE_0:def 5;
cR = the carrier of sum_of(G1,G2) by A5,A9,A6,NECKLA_2:def 3;
hence thesis by A5,A10,A61,A60;
end;
Lm1: for X being non empty finite set, A,B being non empty set st X = A \/ B &
A misses B holds card A in Segm card X
proof
let X be non empty finite set;
let A,B be non empty set;
set n = card X;
assume that
A1: X = A \/ B and
A2: A misses B;
card B c= n by A1,CARD_1:11,XBOOLE_1:7;
then reconsider B as finite set;
card A c= n by A1,CARD_1:11,XBOOLE_1:7;
then reconsider A as finite set;
A3: card B >= 1 by NAT_1:14;
A4: n = card A + card B by A1,A2,CARD_2:40;
card A < n
proof
assume not thesis;
then card A + card B >= n+1 by A3,XREAL_1:7;
hence thesis by A4,NAT_1:13;
end;
hence thesis by NAT_1:44;
end;
theorem
for G being irreflexive RelStr st G in fin_RelStr_sp holds ComplRelStr
G in fin_RelStr_sp
proof
defpred P[Nat] means for G being irreflexive RelStr st card the carrier of G
= $1 & G in fin_RelStr_sp holds ComplRelStr G in fin_RelStr_sp;
let G be irreflexive RelStr;
A1: for k being Nat st for n being Nat st n < k holds P[n] holds P[k]
proof
let k be Nat such that
A2: for n being Nat st n < k holds P[n];
let G be irreflexive RelStr;
assume that
A3: card the carrier of G = k and
A4: G in fin_RelStr_sp;
per cases by A4,NECKLA_2:6;
suppose
G is strict 1-element RelStr;
hence thesis by A4,Th15;
end;
suppose
ex G1,G2 being strict RelStr st (the carrier of G1) misses (the
carrier of G2) & G1 in fin_RelStr_sp & G2 in fin_RelStr_sp & (G = union_of(G1,
G2) or G = sum_of(G1,G2) );
then consider G1,G2 being strict RelStr such that
A5: (the carrier of G1) misses the carrier of G2 and
A6: G1 in fin_RelStr_sp and
A7: G2 in fin_RelStr_sp and
A8: G = union_of(G1,G2) or G = sum_of(G1,G2);
A9: G2 is non empty finite by A7,NECKLA_2:4;
then reconsider n2 = card the carrier of G2 as Nat;
A10: G1 is non empty finite by A6,NECKLA_2:4;
then reconsider n1 = card the carrier of G1 as Nat;
thus thesis
proof
per cases by A8;
suppose
A11: G = union_of(G1,G2);
then reconsider G2 as irreflexive RelStr by Th9;
reconsider G1 as irreflexive RelStr by A11,Th9;
reconsider cG1 = the carrier of G1 as non empty finite set by A10;
reconsider cG2 = the carrier of G2 as non empty finite set by A9;
the carrier of G = (the carrier of G1) \/ the carrier of G2 by A11,
NECKLA_2:def 2;
then
A12: card the carrier of G = card cG1 + card cG2 by A5,CARD_2:40;
A13: card cG1 = n1;
n2 < k
proof
assume not thesis;
then k+0 < n1 + n2 by A13,XREAL_1:8;
hence thesis by A3,A12;
end;
then
A14: ComplRelStr G2 in fin_RelStr_sp by A2,A7;
A15: the carrier of ComplRelStr G1 = the carrier of G1 & the carrier
of ComplRelStr G2 = the carrier of G2 by NECKLACE:def 8;
A16: card cG2 = n2;
n1 < k
proof
assume not thesis;
then k+0 < n2 + n1 by A16,XREAL_1:8;
hence thesis by A3,A12;
end;
then
A17: ComplRelStr G1 in fin_RelStr_sp by A2,A6;
ComplRelStr G = sum_of(ComplRelStr G1,ComplRelStr G2) by A5,A11,Th17;
hence thesis by A5,A17,A14,A15,NECKLA_2:def 5;
end;
suppose
A18: G = sum_of(G1,G2);
then reconsider G2 as irreflexive RelStr by Th9;
reconsider G1 as irreflexive RelStr by A18,Th9;
reconsider cG1 = the carrier of G1 as non empty finite set by A10;
reconsider cG2 = the carrier of G2 as non empty finite set by A9;
the carrier of G = (the carrier of G1) \/ the carrier of G2 by A18,
NECKLA_2:def 3;
then
A19: card the carrier of G = card cG1 + card cG2 by A5,CARD_2:40;
A20: card cG1 = n1;
n2 < k
proof
assume not thesis;
then k+0 < n1 + n2 by A20,XREAL_1:8;
hence thesis by A3,A19;
end;
then
A21: ComplRelStr G2 in fin_RelStr_sp by A2,A7;
A22: the carrier of ComplRelStr G1 = the carrier of G1 & the carrier
of ComplRelStr G2 = the carrier of G2 by NECKLACE:def 8;
A23: card cG2 = n2;
n1 < k
proof
assume not thesis;
then k+0 < n2 + n1 by A23,XREAL_1:8;
hence thesis by A3,A19;
end;
then
A24: ComplRelStr G1 in fin_RelStr_sp by A2,A6;
ComplRelStr G = union_of(ComplRelStr G1,ComplRelStr G2) by A5,A18
,Th18;
hence thesis by A5,A24,A21,A22,NECKLA_2:def 5;
end;
end;
end;
end;
A25: for k being Nat holds P[k] from NAT_1:sch 4(A1);
assume
A26: G in fin_RelStr_sp;
then G is finite by NECKLA_2:4;
then card the carrier of G is Nat;
hence thesis by A26,A25;
end;
theorem Th33:
for R be irreflexive symmetric RelStr st card (the carrier of R)
= 2 & the carrier of R in FinSETS holds the RelStr of R in fin_RelStr_sp
proof
let R be irreflexive symmetric RelStr;
assume that
A1: card (the carrier of R) = 2 and
A2: the carrier of R in FinSETS;
consider a,b being object such that
A3: the carrier of R = {a,b} and
A4: the InternalRel of R = {[a,b],[b,a]} or the InternalRel of R = {}
by A1,Th6;
set A = {a}, B = {b};
A5: A c= the carrier of R
proof
let x be object;
assume x in A;
then x = a by TARSKI:def 1;
hence thesis by A3,TARSKI:def 2;
end;
A6: B c= the carrier of R
proof
let x be object;
assume x in B;
then x = b by TARSKI:def 1;
hence thesis by A3,TARSKI:def 2;
end;
then reconsider B as Subset of R;
reconsider A as Subset of R by A5;
set H1 = subrelstr A, H2 = subrelstr B;
reconsider H2 as non empty strict irreflexive symmetric RelStr by
YELLOW_0:def 15;
A7: the carrier of H2 = B by YELLOW_0:def 15;
then the InternalRel of H2 c= [:{b},{b}:];
then the InternalRel of H2 c= {[b,b]} by ZFMISC_1:29;
then
A8: the InternalRel of H2 = {} or the InternalRel of H2 = {[b,b]} by
ZFMISC_1:33;
A9: the InternalRel of H2 = {}
proof
b in B by TARSKI:def 1;
then b in the carrier of H2 by YELLOW_0:def 15;
then
A10: not [b,b] in the InternalRel of H2 by NECKLACE:def 5;
assume not thesis;
hence thesis by A8,A10,TARSKI:def 1;
end;
the carrier of H2 c= the carrier of R by A6,YELLOW_0:def 15;
then the carrier of H2 in FinSETS by A2,CLASSES1:3,CLASSES2:def 2;
then
A11: H2 in fin_RelStr_sp by A7,NECKLA_2:def 5;
reconsider H1 as non empty strict irreflexive symmetric RelStr by
YELLOW_0:def 15;
A12: the carrier of H1 = A by YELLOW_0:def 15;
then
A13: the carrier of R = (the carrier of H1) \/ (the carrier of H2) by A3,A7,
ENUMSET1:1;
a <> b
proof
assume not thesis;
then the carrier of R = {a} by A3,ENUMSET1:29;
hence thesis by A1,CARD_1:30;
end;
then
A14: A misses B by ZFMISC_1:11;
then
A15: (the carrier of H1) misses (the carrier of H2) by A7,YELLOW_0:def 15;
the InternalRel of H1 c= [:{a},{a}:] by A12;
then the InternalRel of H1 c= {[a,a]} by ZFMISC_1:29;
then
A16: the InternalRel of H1 = {} or the InternalRel of H1 = {[a,a]} by
ZFMISC_1:33;
A17: the InternalRel of H1 = {}
proof
a in A by TARSKI:def 1;
then a in the carrier of H1 by YELLOW_0:def 15;
then
A18: not [a,a] in the InternalRel of H1 by NECKLACE:def 5;
assume not thesis;
hence thesis by A16,A18,TARSKI:def 1;
end;
the carrier of H1 c= the carrier of R by A5,YELLOW_0:def 15;
then the carrier of H1 in FinSETS by A2,CLASSES1:3,CLASSES2:def 2;
then
A19: H1 in fin_RelStr_sp by A12,NECKLA_2:def 5;
per cases by A4;
suppose
A20: the InternalRel of R = {[a,b],[b,a]};
set S = sum_of(H1,H2);
the InternalRel of S = (the InternalRel of H1) \/ (the InternalRel of
H2) \/ [:A,B:] \/ [:B,A:] by A12,A7,NECKLA_2:def 3;
then the InternalRel of S = {[a,b]} \/ [:{b},{a}:] by A17,A9,ZFMISC_1:29;
then the InternalRel of S = {[a,b]} \/ {[b,a]} by ZFMISC_1:29;
then
A21: the InternalRel of S = the InternalRel of R by A20,ENUMSET1:1;
the carrier of S = the carrier of R by A13,NECKLA_2:def 3;
hence thesis by A12,A19,A7,A11,A14,A21,NECKLA_2:def 5;
end;
suppose
A22: the InternalRel of R = {};
set U = union_of(H1,H2);
the InternalRel of U = (the InternalRel of H1) \/ (the InternalRel of
H2 ) & the carrier of U = the carrier of R by A13,NECKLA_2:def 2;
hence thesis by A19,A11,A15,A17,A9,A22,NECKLA_2:def 5;
end;
end;
theorem
for R be RelStr st R in fin_RelStr_sp holds R is symmetric
proof
let X be RelStr;
assume
A1: X in fin_RelStr_sp;
per cases;
suppose
A2: X is trivial;
thus thesis
proof
per cases by A2,ZFMISC_1:131;
suppose
A3: the carrier of X is empty;
let a,b be object;
assume that
A4: a in the carrier of X and
b in the carrier of X and
[a,b] in the InternalRel of X;
thus thesis by A3,A4;
end;
suppose
ex x being object st the carrier of X = {x};
then consider x being object such that
A5: the carrier of X = {x};
A6: [:the carrier of X,the carrier of X:] = {[x,x]} by A5,ZFMISC_1:29;
thus thesis
proof
per cases by A6,ZFMISC_1:33;
suppose
A7: the InternalRel of X = {};
let a,b be object;
assume that
a in the carrier of X and
b in the carrier of X and
A8: [a,b] in the InternalRel of X;
thus thesis by A7,A8;
end;
suppose
A9: the InternalRel of X = {[x,x]};
let a,b be object;
assume that
a in the carrier of X and
b in the carrier of X and
A10: [a,b] in the InternalRel of X;
A11: [a,b] = [x,x] by A9,A10,TARSKI:def 1;
then a = x by XTUPLE_0:1;
hence thesis by A10,A11,XTUPLE_0:1;
end;
end;
end;
end;
end;
suppose
A12: not X is trivial;
defpred P[Nat] means for X be non empty RelStr st not X is trivial & X in
fin_RelStr_sp holds card (the carrier of X) c= $1 implies X is symmetric;
A13: ex R be strict RelStr st X = R & the carrier of R in FinSETS by A1,
NECKLA_2:def 4;
reconsider X as non empty RelStr by A1,NECKLA_2:4;
A14: card the carrier of X is Nat by A13;
A15: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A16: P[k];
reconsider k1=k as Element of NAT by ORDINAL1:def 12;
let Y be non empty RelStr such that
A17: not Y is trivial and
A18: Y in fin_RelStr_sp;
consider H1,H2 be strict RelStr such that
A19: the carrier of H1 misses the carrier of H2 and
A20: H1 in fin_RelStr_sp and
A21: H2 in fin_RelStr_sp and
A22: Y = union_of(H1,H2) or Y = sum_of(H1,H2) by A17,A18,NECKLA_2:6;
ex R be strict RelStr st Y = R & the carrier of R in FinSETS by A18,
NECKLA_2:def 4;
then reconsider cY = the carrier of Y as finite set;
assume card (the carrier of Y) c= k+1;
then Segm card cY c= Segm card (k1+1);
then card cY <= card (k1+1) by NAT_1:39;
then
A23: card cY <= k+1;
set cH1 = the carrier of H1, cH2 = the carrier of H2;
A24: card cY = card ((cH1) \/ cH2) by A22,NECKLA_2:def 2,def 3;
ex R2 be strict RelStr st H2 = R2 & the carrier of R2 in FinSETS by A21,
NECKLA_2:def 4;
then reconsider cH2 as finite set;
ex R1 be strict RelStr st H1 = R1 & the carrier of R1 in FinSETS by A20,
NECKLA_2:def 4;
then reconsider cH1 as finite set;
A25: card cY = card cH1 + card cH2 by A19,A24,CARD_2:40;
H1 is non empty by A20,NECKLA_2:4;
then
A26: card cH1 >= 1 by NAT_1:14;
H2 is non empty by A21,NECKLA_2:4;
then
A27: card cH2 >= 1 by NAT_1:14;
per cases by A25,A23,A26,A27,NAT_1:8,XXREAL_0:1;
suppose
card cY <= k;
then card cY <= card k1;
then Segm card cY c= Segm card k by NAT_1:39;
then card (the carrier of Y) c= k1;
hence thesis by A16,A17,A18;
end;
suppose
A28: card cY = k+1 & k = 0;
set x = the set;
card cY = card {x} by A28,CARD_1:30;
then cY,{x} are_equipotent by CARD_1:5;
then ex y being object st cY = {y} by CARD_1:28;
hence thesis by A17;
end;
suppose
A29: card cH1 + card cH2 = k+1 & k > 0 & card cH1 = 1 & card cH2 = 1;
then ex x be object st cH1 = {x} by CARD_2:42;
then the InternalRel of H1 is_symmetric_in cH1 by Th5;
then reconsider H1 as symmetric RelStr by NECKLACE:def 3;
ex y be object st cH2 = {y} by A29,CARD_2:42;
then the InternalRel of H2 is_symmetric_in cH2 by Th5;
then reconsider H2 as symmetric RelStr by NECKLACE:def 3;
union_of(H1,H2) is symmetric;
hence thesis by A22;
end;
suppose
A30: card cH1 + card cH2 = k+1 & k > 0 & card cH1 = 1 & card cH2 > 1;
then ex x be object st cH1 = {x} by CARD_2:42;
then the InternalRel of H1 is_symmetric_in cH1 by Th5;
then reconsider H1 as symmetric RelStr by NECKLACE:def 3;
card cH2 is non trivial by A30,NAT_2:28;
then card cH2 >= 2 by NAT_2:29;
then H2 is non empty non trivial by NAT_D:60;
then reconsider H2 as symmetric RelStr by A16,A21,A30;
union_of(H1,H2) is symmetric;
hence thesis by A22;
end;
suppose
A31: card cH1 + card cH2 = k+1 & k > 0 & card cH1 > 1 & card cH2 = 1;
then ex x be object st cH2 = {x} by CARD_2:42;
then the InternalRel of H2 is_symmetric_in cH2 by Th5;
then reconsider H2 as symmetric RelStr by NECKLACE:def 3;
card cH1 is non trivial by A31,NAT_2:28;
then card cH1 >= 2 by NAT_2:29;
then H1 is non empty non trivial by NAT_D:60;
then reconsider H1 as symmetric RelStr by A16,A20,A31;
union_of(H1,H2) is symmetric;
hence thesis by A22;
end;
suppose
A32: card cH1 + card cH2 = k+1 & k > 0 & card cH1 > 1 & card cH2 > 1;
then card cH2 is non trivial by NAT_2:28;
then card cH2 >= 2 by NAT_2:29;
then
A33: H2 is non empty non trivial by NAT_D:60;
card cH2 < k+1
proof
assume not thesis;
then card cH1 + card cH2 >= (k+1)+1 by A26,XREAL_1:7;
hence thesis by A32,NAT_1:13;
end;
then card cH2 <= k by NAT_1:13;
then card cH2 <= card k1;
then Segm card cH2 c= Segm card k by NAT_1:39;
then card cH2 c= k1;
then reconsider H2 as symmetric RelStr by A16,A21,A33;
card cH1 is non trivial by A32,NAT_2:28;
then card cH1 >= 2 by NAT_2:29;
then
A34: H1 is non empty non trivial by NAT_D:60;
card cH1 < k+1
proof
assume not thesis;
then card cH1 + card cH2 >= (k+1)+1 by A27,XREAL_1:7;
hence thesis by A32,NAT_1:13;
end;
then card cH1 <= k by NAT_1:13;
then card cH1 <= card k1;
then Segm card cH1 c= Segm card k by NAT_1:39;
then card cH1 c= k1;
then reconsider H1 as symmetric RelStr by A16,A20,A34;
union_of(H1,H2) is symmetric;
hence thesis by A22;
end;
end;
A35: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A35,A15);
hence thesis by A1,A12,A14;
end;
end;
theorem Th35:
for G being RelStr, H1,H2 being non empty RelStr, x being
Element of H1, y being Element of H2 st G = union_of(H1,H2) & the carrier of H1
misses the carrier of H2 holds not [x,y] in the InternalRel of G
proof
let G be RelStr;
let H1,H2 be non empty RelStr;
let x be Element of H1;
let y be Element of H2;
assume that
A1: G = union_of(H1,H2) and
A2: (the carrier of H1) misses (the carrier of H2);
assume not thesis;
then
A3: [x,y] in (the InternalRel of H1) \/ the InternalRel of H2 by A1,
NECKLA_2:def 2;
per cases by A3,XBOOLE_0:def 3;
suppose
[x,y] in (the InternalRel of H1);
then y in the carrier of H1 by ZFMISC_1:87;
then y in (the carrier of H1) /\ the carrier of H2 by XBOOLE_0:def 4;
hence thesis by A2;
end;
suppose
[x,y] in (the InternalRel of H2);
then x in the carrier of H2 by ZFMISC_1:87;
then x in (the carrier of H1) /\ the carrier of H2 by XBOOLE_0:def 4;
hence thesis by A2;
end;
end;
theorem
for G being RelStr, H1,H2 being non empty RelStr, x being Element of
H1, y being Element of H2 st G = sum_of(H1,H2) holds not [x,y] in the
InternalRel of ComplRelStr G
proof
let G being RelStr,H1,H2 being non empty RelStr, x being Element of H1, y
being Element of H2;
set cH1 = the carrier of H1, cH2 = the carrier of H2, IH1 = the InternalRel
of H1, IH2 = the InternalRel of H2;
[x,y] in [:cH1,cH2:] \/ [:cH2,cH1:] by XBOOLE_0:def 3;
then [x,y] in IH2 \/ ([:cH1,cH2:] \/ [:cH2,cH1:]) by XBOOLE_0:def 3;
then [x,y] in IH1 \/ (IH2 \/ ([:cH1,cH2:] \/ [:cH2,cH1:])) by XBOOLE_0:def 3;
then [x,y] in IH1 \/ (IH2 \/ [:cH1,cH2:] \/ [:cH2,cH1:]) by XBOOLE_1:4;
then
A1: [x,y] in IH1 \/ IH2 \/ [:cH1,cH2:] \/ [:cH2,cH1:] by XBOOLE_1:113;
assume G = sum_of(H1,H2);
then
A2: [x,y] in the InternalRel of G by A1,NECKLA_2:def 3;
not [x,y] in the InternalRel of ComplRelStr G
proof
assume not thesis;
then [x,y] in (the InternalRel of G) /\ the InternalRel of ComplRelStr G
by A2,XBOOLE_0:def 4;
then (the InternalRel of G) meets the InternalRel of ComplRelStr G;
hence contradiction by Th12;
end;
hence thesis;
end;
theorem Th37:
for G being non empty symmetric RelStr, x being Element of G, R1
,R2 being non empty RelStr st the carrier of R1 misses the carrier of R2 &
subrelstr ([#]G \ {x}) = union_of(R1,R2) & G is path-connected holds ex b being
Element of R1 st [b,x] in the InternalRel of G
proof
let G be non empty symmetric RelStr;
let x be Element of G;
let R1,R2 be non empty RelStr;
assume that
A1: the carrier of R1 misses the carrier of R2 and
A2: subrelstr ([#]G \ {x}) = union_of(R1,R2) and
A3: G is path-connected;
set R = subrelstr ([#]G \ {x}), A = the carrier of R;
the carrier of R1 c= (the carrier of R1) \/ the carrier of R2 by XBOOLE_1:7;
then
A4: the carrier of R1 c= the carrier of R by A2,NECKLA_2:def 2;
set a = the Element of R1;
A5: A = [#]G \ {x} by YELLOW_0:def 15;
A6: x <> a
proof
assume not thesis;
then x in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
then x in (the carrier of G) \ {x} by A2,A5,NECKLA_2:def 2;
then not x in {x} by XBOOLE_0:def 5;
hence thesis by TARSKI:def 1;
end;
reconsider A as Subset of G by YELLOW_0:def 15;
A7: the carrier of R = A;
then the carrier of R1 c= the carrier of G by A4,XBOOLE_1:1;
then a in the carrier of G;
then (the InternalRel of G) reduces x,a by A3,A6;
then consider p being FinSequence such that
A8: len p > 0 and
A9: p.1 = x and
A10: p.len p = a and
A11: for i being Nat st i in dom p & i+1 in dom p holds [p.i,
p.(i+1)] in (the InternalRel of G) by REWRITE1:11;
defpred P[Nat] means p.$1 in the carrier of R1 & $1 in dom p & for k being
Nat st k > $1 holds k in dom p implies p.k in the carrier of R1;
P[len p] by A8,A10,CARD_1:27,FINSEQ_3:25,FINSEQ_5:6;
then
A12: ex k being Nat st P[k];
ex n0 being Nat st P[n0] & for n being Nat st P[n] holds n >= n0 from
NAT_1:sch 5(A12);
then consider n0 being Element of NAT such that
A13: P[n0] and
A14: for n being Nat st P[n] holds n >= n0;
n0 <> 0
proof
assume not thesis;
then 0 in Seg (len p) by A13,FINSEQ_1:def 3;
hence contradiction by FINSEQ_1:1;
end;
then consider k0 being Nat such that
A15: n0 = k0 + 1 by NAT_1:6;
A16: n0 <> 1
proof
assume not thesis;
then not x in {x} by A5,A4,A9,A13,XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1;
end;
A17: k0 >= 1
proof
assume not thesis;
then k0 = 0 by NAT_1:25;
hence contradiction by A15,A16;
end;
n0 in Seg (len p) by A13,FINSEQ_1:def 3;
then
A18: n0 <= len p by FINSEQ_1:1;
A19: k0 < n0 by A15,NAT_1:13;
A20: for k being Nat st k > k0 holds k in dom p implies p.k in the carrier
of R1
proof
assume not thesis;
then consider k being Nat such that
A21: k > k0 and
A22: k in dom p and
A23: not p.k in the carrier of R1;
k > n0
proof
per cases by XXREAL_0:1;
suppose
k < n0;
hence thesis by A15,A21,NAT_1:13;
end;
suppose
n0 < k;
hence thesis;
end;
suppose
n0 = k;
hence thesis by A13,A23;
end;
end;
hence contradiction by A13,A22,A23;
end;
A24: the carrier of G = (the carrier of R) \/ {x}
proof
thus the carrier of G c= (the carrier of R) \/ {x}
proof
let a be object;
assume
A25: a in the carrier of G;
per cases;
suppose
a = x;
then a in {x} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
a <> x;
then not a in {x} by TARSKI:def 1;
then a in A by A5,A25,XBOOLE_0:def 5;
hence thesis by XBOOLE_0:def 3;
end;
end;
let a be object;
assume
A26: a in (the carrier of R) \/ {x};
per cases by A26,XBOOLE_0:def 3;
suppose
a in the carrier of R;
hence thesis by A5;
end;
suppose
a in {x};
hence thesis;
end;
end;
k0 <= n0 by A15,XREAL_1:29;
then k0 <= len p by A18,XXREAL_0:2;
then
A27: k0 in dom p by A17,FINSEQ_3:25;
then
A28: [p.k0,p.(k0+1)] in the InternalRel of G by A11,A13,A15;
then
A29: p.k0 in the carrier of G by ZFMISC_1:87;
thus thesis
proof
per cases by A29,A24,XBOOLE_0:def 3;
suppose
A30: p.k0 in the carrier of R;
set u = p.k0, v = p.n0;
[u,v] in [:the carrier of R,the carrier of R:] by A4,A13,A30,ZFMISC_1:87;
then
A31: [u,v] in (the InternalRel of G)|_2 the carrier of R by A15,A28,
XBOOLE_0:def 4;
p.k0 in (the carrier of R1) \/ the carrier of R2 by A2,A30,NECKLA_2:def 2
;
then p.k0 in the carrier of R1 or p.k0 in the carrier of R2 by
XBOOLE_0:def 3;
then reconsider u as Element of R2 by A14,A27,A19,A20;
reconsider v as Element of R1 by A13;
not [u,v] in the InternalRel of R
proof
u in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
then
A32: u in the carrier of R by A2,NECKLA_2:def 2;
A33: v in the carrier of R1 & the InternalRel of R is_symmetric_in the
carrier of R by NECKLACE:def 3;
assume not thesis;
then [v,u] in the InternalRel of R by A4,A32,A33;
hence thesis by A1,A2,Th35;
end;
hence thesis by A31,YELLOW_0:def 14;
end;
suppose
A34: p.k0 in {x};
set b = p.n0;
reconsider b as Element of R1 by A13;
A35: b in the carrier of R & (the InternalRel of G) is_symmetric_in the
carrier of G by A4,NECKLACE:def 3;
p.k0 = x by A34,TARSKI:def 1;
then [b,x] in (the InternalRel of G) by A7,A15,A28,A35;
hence thesis;
end;
end;
end;
theorem Th38:
for G being non empty symmetric irreflexive RelStr, a,b,c,d
being Element of G, Z being Subset of G st Z = {a,b,c,d} & a,b,c,d
are_mutually_distinct & [a,b] in the InternalRel of G & [b,c] in the
InternalRel of G & [c,d] in the InternalRel of G & not [a,c] in the InternalRel
of G & not [a,d] in the InternalRel of G & not [b,d] in the InternalRel of G
holds subrelstr Z embeds Necklace 4
proof
let G be non empty symmetric irreflexive symmetric RelStr;
let a,b,c,d be Element of G;
let Z be Subset of G;
assume that
A1: Z = {a,b,c,d} and
A2: a,b,c,d are_mutually_distinct and
A3: [a,b] in the InternalRel of G and
A4: [b,c] in the InternalRel of G and
A5: [c,d] in the InternalRel of G and
A6: not [a,c] in the InternalRel of G and
A7: not [a,d] in the InternalRel of G and
A8: not [b,d] in the InternalRel of G;
set g = (0,1) --> (a,b), h = (2,3) --> (c,d), f = g +* h;
A9: rng h = {c,d} by FUNCT_4:64;
A10: a <> b by A2,ZFMISC_1:def 6;
A11: rng (0 .--> a) misses rng (1 .--> b)
proof
assume rng (0 .--> a) meets rng (1 .--> b);
then consider x being object such that
A12: x in rng (0 .--> a) and
A13: x in rng (1 .--> b) by XBOOLE_0:3;
rng (0 .--> a) = {a} by FUNCOP_1:8;
then rng (1 .--> b) = {b} & x = a by A12,FUNCOP_1:8,TARSKI:def 1;
hence contradiction by A10,A13,TARSKI:def 1;
end;
set H = subrelstr Z, N4 = Necklace 4, IH = the InternalRel of H, cH = the
carrier of H, IG = the InternalRel of G, X = {[a,a],[a,b],[b,a],[b,b],[a,c],[a,
d],[b,c],[b,d]}, Y = {[c,a],[c,b],[d,a],[d,b],[c,c],[c,d],[d,c],[d,d]};
A14: the carrier of H is non empty by A1,YELLOW_0:def 15;
A15: h = (2 .--> c) +* (3 .--> d) by FUNCT_4:def 4;
A16: c <> d by A2,ZFMISC_1:def 6;
rng (2 .--> c) misses rng (3 .--> d)
proof
assume rng (2 .--> c) meets rng (3 .--> d);
then consider x being object such that
A17: x in rng (2 .--> c) and
A18: x in rng (3 .--> d) by XBOOLE_0:3;
rng (2 .--> c) = {c} by FUNCOP_1:8;
then rng (3 .--> d) = {d} & x = c by A17,FUNCOP_1:8,TARSKI:def 1;
hence contradiction by A16,A18,TARSKI:def 1;
end;
then
A19: h is one-to-one by A15,FUNCT_4:92;
A20: rng g = {a,b} by FUNCT_4:64;
A21: rng g misses rng h
proof
assume not thesis;
then consider x being object such that
A22: x in rng g and
A23: x in rng h by XBOOLE_0:3;
A24: x = c or x = d by A9,A23,TARSKI:def 2;
x = a or x = b by A20,A22,TARSKI:def 2;
hence contradiction by A2,A24,ZFMISC_1:def 6;
end;
dom f = dom g \/ dom h by FUNCT_4:def 1
.= {0,1} \/ dom h by FUNCT_4:62
.= {0,1} \/ {2,3} by FUNCT_4:62
.= {0,1,2,3} by ENUMSET1:5;
then
A25: dom f = the carrier of N4 by NECKLACE:1,20;
A26: dom g misses dom h
proof
assume not thesis;
then consider x being object such that
A27: x in dom g and
A28: x in dom h by XBOOLE_0:3;
x=0 or x=1 by A27,TARSKI:def 2;
hence contradiction by A28,TARSKI:def 2;
end;
then rng f = rng g \/ rng h by NECKLACE:6;
then rng f = {a,b,c,d} by A20,A9,ENUMSET1:5;
then
A29: rng f = the carrier of H by A1,YELLOW_0:def 15;
then reconsider f as Function of N4,H by A25,FUNCT_2:def 1,RELSET_1:4;
g = (0 .--> a) +* (1 .-->b) by FUNCT_4:def 4;
then
A30: g is one-to-one by A11,FUNCT_4:92;
then
A31: f is one-to-one by A19,A21,FUNCT_4:92;
A32: the InternalRel of H = {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
proof
thus the InternalRel of H c= {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
proof
let x be object;
A33: the carrier of H = Z by YELLOW_0:def 15;
assume
A34: x in IH;
then
A35: x in IG |_2 cH by YELLOW_0:def 14;
then
A36: x in IG by XBOOLE_0:def 4;
x in [:cH,cH:] by A34;
then
A37: x in X \/ Y by A1,A33,Th3;
per cases by A37,XBOOLE_0:def 3;
suppose
A38: x in X;
thus thesis
proof
per cases by A38,ENUMSET1:def 6;
suppose
A39: x = [a,a];
not [a,a] in IG by NECKLACE:def 5;
hence thesis by A35,A39,XBOOLE_0:def 4;
end;
suppose
x =[a,b];
hence thesis by ENUMSET1:def 4;
end;
suppose
x =[b,a];
hence thesis by ENUMSET1:def 4;
end;
suppose
A40: x =[b,b];
not [b,b] in IG by NECKLACE:def 5;
hence thesis by A35,A40,XBOOLE_0:def 4;
end;
suppose
x = [a,c];
hence thesis by A6,A35,XBOOLE_0:def 4;
end;
suppose
x = [a,d];
hence thesis by A7,A35,XBOOLE_0:def 4;
end;
suppose
x = [b,c];
hence thesis by ENUMSET1:def 4;
end;
suppose
x =[b,d];
hence thesis by A8,A35,XBOOLE_0:def 4;
end;
end;
end;
suppose
A41: x in Y;
A42: IG is_symmetric_in the carrier of G by NECKLACE:def 3;
thus thesis
proof
per cases by A41,ENUMSET1:def 6;
suppose
x = [c,a];
hence thesis by A6,A36,A42;
end;
suppose
x = [c,b];
hence thesis by ENUMSET1:def 4;
end;
suppose
x = [d,a];
hence thesis by A7,A36,A42;
end;
suppose
x = [d,b];
hence thesis by A8,A36,A42;
end;
suppose
A43: x = [c,c];
not [c,c] in IG by NECKLACE:def 5;
hence thesis by A35,A43,XBOOLE_0:def 4;
end;
suppose
x = [c,d];
hence thesis by ENUMSET1:def 4;
end;
suppose
x = [d,c];
hence thesis by ENUMSET1:def 4;
end;
suppose
A44: x = [d,d];
not [d,d] in IG by NECKLACE:def 5;
hence thesis by A35,A44,XBOOLE_0:def 4;
end;
end;
end;
end;
let x be object;
assume
A45: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]};
per cases by A45,ENUMSET1:def 4;
suppose
A46: x = [a,b];
b in Z by A1,ENUMSET1:def 2;
then
A47: b in cH by YELLOW_0:def 15;
a in Z by A1,ENUMSET1:def 2;
then a in cH by YELLOW_0:def 15;
then [a,b] in [:cH,cH:] by A47,ZFMISC_1:87;
then x in IG |_2 cH by A3,A46,XBOOLE_0:def 4;
hence thesis by YELLOW_0:def 14;
end;
suppose
A48: x = [b,a];
IG is_symmetric_in the carrier of G by NECKLACE:def 3;
then
A49: [b,a] in IG by A3;
a in Z by A1,ENUMSET1:def 2;
then
A50: a in cH by YELLOW_0:def 15;
b in Z by A1,ENUMSET1:def 2;
then b in cH by YELLOW_0:def 15;
then [b,a] in [:cH,cH:] by A50,ZFMISC_1:87;
then x in IG |_2 cH by A48,A49,XBOOLE_0:def 4;
hence thesis by YELLOW_0:def 14;
end;
suppose
A51: x = [b,c];
c in Z by A1,ENUMSET1:def 2;
then
A52: c in cH by YELLOW_0:def 15;
b in Z by A1,ENUMSET1:def 2;
then b in cH by YELLOW_0:def 15;
then [b,c] in [:cH,cH:] by A52,ZFMISC_1:87;
then x in IG |_2 cH by A4,A51,XBOOLE_0:def 4;
hence thesis by YELLOW_0:def 14;
end;
suppose
A53: x = [c,b];
IG is_symmetric_in the carrier of G by NECKLACE:def 3;
then
A54: [c,b] in IG by A4;
c in Z by A1,ENUMSET1:def 2;
then
A55: c in cH by YELLOW_0:def 15;
b in Z by A1,ENUMSET1:def 2;
then b in cH by YELLOW_0:def 15;
then [c,b] in [:cH,cH:] by A55,ZFMISC_1:87;
then x in IG |_2 cH by A53,A54,XBOOLE_0:def 4;
hence thesis by YELLOW_0:def 14;
end;
suppose
A56: x = [c,d];
d in Z by A1,ENUMSET1:def 2;
then
A57: d in cH by YELLOW_0:def 15;
c in Z by A1,ENUMSET1:def 2;
then c in cH by YELLOW_0:def 15;
then [c,d] in [:cH,cH:] by A57,ZFMISC_1:87;
then x in IG |_2 cH by A5,A56,XBOOLE_0:def 4;
hence thesis by YELLOW_0:def 14;
end;
suppose
A58: x = [d,c];
IG is_symmetric_in the carrier of G by NECKLACE:def 3;
then
A59: [d,c] in IG by A5;
d in Z by A1,ENUMSET1:def 2;
then
A60: d in cH by YELLOW_0:def 15;
c in Z by A1,ENUMSET1:def 2;
then c in cH by YELLOW_0:def 15;
then [d,c] in [:cH,cH:] by A60,ZFMISC_1:87;
then x in IG |_2 cH by A58,A59,XBOOLE_0:def 4;
hence thesis by YELLOW_0:def 14;
end;
end;
for x,y being Element of N4 holds [x,y] in the InternalRel of N4 iff [
f.x,f.y] in the InternalRel of H
proof
let x,y being Element of N4;
thus [x,y] in the InternalRel of N4 implies [f.x,f.y] in the InternalRel
of H
proof
assume
A61: [x,y] in the InternalRel of N4;
per cases by A61,ENUMSET1:def 4,NECKLA_2:2;
suppose
A62: [x,y] = [0,1];
then
A63: y = 1 by XTUPLE_0:1;
then y in {0,1} by TARSKI:def 2;
then y in dom g by FUNCT_4:62;
then
A64: f.y = g.1 by A26,A63,FUNCT_4:16
.= b by FUNCT_4:63;
A65: x = 0 by A62,XTUPLE_0:1;
then x in {0,1} by TARSKI:def 2;
then x in dom g by FUNCT_4:62;
then f.x = g.0 by A26,A65,FUNCT_4:16
.= a by FUNCT_4:63;
hence thesis by A32,A64,ENUMSET1:def 4;
end;
suppose
A66: [x,y] = [1,0];
then
A67: y = 0 by XTUPLE_0:1;
then y in {0,1} by TARSKI:def 2;
then y in dom g by FUNCT_4:62;
then
A68: f.y = g.0 by A26,A67,FUNCT_4:16
.= a by FUNCT_4:63;
A69: x = 1 by A66,XTUPLE_0:1;
then x in {0,1} by TARSKI:def 2;
then x in dom g by FUNCT_4:62;
then f.x = g.1 by A26,A69,FUNCT_4:16
.= b by FUNCT_4:63;
hence thesis by A32,A68,ENUMSET1:def 4;
end;
suppose
A70: [x,y] = [1,2];
then
A71: x = 1 by XTUPLE_0:1;
then x in {0,1} by TARSKI:def 2;
then x in dom g by FUNCT_4:62;
then
A72: f.x = g.1 by A26,A71,FUNCT_4:16
.= b by FUNCT_4:63;
A73: y = 2 by A70,XTUPLE_0:1;
then y in {2,3} by TARSKI:def 2;
then
A74: y in dom h by FUNCT_4:62;
g +* h = h +* g by A26,FUNCT_4:35;
then f.y = h.2 by A26,A73,A74,FUNCT_4:16
.= c by FUNCT_4:63;
hence thesis by A32,A72,ENUMSET1:def 4;
end;
suppose
A75: [x,y] = [2,1];
then
A76: y = 1 by XTUPLE_0:1;
then y in {0,1} by TARSKI:def 2;
then y in dom g by FUNCT_4:62;
then
A77: f.y = g.1 by A26,A76,FUNCT_4:16
.= b by FUNCT_4:63;
A78: x = 2 by A75,XTUPLE_0:1;
then x in {2,3} by TARSKI:def 2;
then
A79: x in dom h by FUNCT_4:62;
g +* h = h +* g by A26,FUNCT_4:35;
then f.x = h.2 by A26,A78,A79,FUNCT_4:16
.= c by FUNCT_4:63;
hence thesis by A32,A77,ENUMSET1:def 4;
end;
suppose
A80: [x,y] = [2,3];
A81: g +* h = h +* g by A26,FUNCT_4:35;
A82: y = 3 by A80,XTUPLE_0:1;
then y in {2,3} by TARSKI:def 2;
then y in dom h by FUNCT_4:62;
then
A83: f.y = h.3 by A26,A82,A81,FUNCT_4:16
.= d by FUNCT_4:63;
A84: x = 2 by A80,XTUPLE_0:1;
then x in {2,3} by TARSKI:def 2;
then x in dom h by FUNCT_4:62;
then f.x = h.2 by A26,A84,A81,FUNCT_4:16
.= c by FUNCT_4:63;
hence thesis by A32,A83,ENUMSET1:def 4;
end;
suppose
A85: [x,y] = [3,2];
A86: g +* h = h +* g by A26,FUNCT_4:35;
A87: y = 2 by A85,XTUPLE_0:1;
then y in {3,2} by TARSKI:def 2;
then y in dom h by FUNCT_4:62;
then
A88: f.y = h.2 by A26,A87,A86,FUNCT_4:16
.= c by FUNCT_4:63;
A89: x = 3 by A85,XTUPLE_0:1;
then x in {3,2} by TARSKI:def 2;
then x in dom h by FUNCT_4:62;
then f.x = h.3 by A26,A89,A86,FUNCT_4:16
.= d by FUNCT_4:63;
hence thesis by A32,A88,ENUMSET1:def 4;
end;
end;
thus [f.x,f.y] in the InternalRel of H implies [x,y] in the InternalRel of
N4
proof
reconsider F=f" as Function of the carrier of H,the carrier of N4 by A29
,A31,FUNCT_2:25;
A90: dom g = {0,1} by FUNCT_4:62;
A91: rng g = {a,b} by FUNCT_4:64;
then reconsider g as Function of {0,1},{a,b} by A90,RELSET_1:4;
reconsider G = g" as Function of {a,b},{0,1} by A20,A30,FUNCT_2:25;
A92: dom h = {2,3} by FUNCT_4:62;
A93: rng h = {c,d} by FUNCT_4:64;
then reconsider h as Function of {2,3},{c,d} by A92,RELSET_1:4;
reconsider Hh = h" as Function of {c,d},{2,3} by A9,A19,FUNCT_2:25;
A94: dom Hh = {c,d} by A19,A93,FUNCT_1:33;
A95: Hh = (c,d) --> (2,3) by A16,NECKLACE:10;
A96: F = G +* Hh by A26,A30,A19,A21,NECKLACE:7;
A97: G = (a,b) --> (0,1) by A10,NECKLACE:10;
A98: dom G = {a,b} by A30,A91,FUNCT_1:33;
then G +* Hh = Hh +* G by A20,A9,A21,A94,FUNCT_4:35;
then
A99: F = Hh +* G by A26,A30,A19,A21,NECKLACE:7;
assume
A100: [f.x,f.y] in the InternalRel of H;
per cases by A32,A100,ENUMSET1:def 4;
suppose
A101: [f.x,f.y] = [a,b];
then
A102: f.x = a by XTUPLE_0:1;
then f.x in {a,b} by TARSKI:def 2;
then F.(f.x) = G.a by A20,A9,A21,A98,A94,A96,A102,FUNCT_4:16
.= 0 by A10,A97,FUNCT_4:63;
then
A103: x = 0 by A14,A31,FUNCT_2:26;
A104: f.y = b by A101,XTUPLE_0:1;
then f.y in dom G by A98,TARSKI:def 2;
then
A105: F.(f.y) = G.b by A20,A9,A21,A98,A94,A96,A104,FUNCT_4:16
.= 1 by A97,FUNCT_4:63;
F.(f.y) = y by A14,A31,FUNCT_2:26;
hence thesis by A103,A105,ENUMSET1:def 4,NECKLA_2:2;
end;
suppose
A106: [f.x,f.y] = [b,a];
then
A107: f.y = a by XTUPLE_0:1;
then f.y in {a,b} by TARSKI:def 2;
then F.(f.y) = G.a by A20,A9,A21,A98,A94,A96,A107,FUNCT_4:16
.= 0 by A10,A97,FUNCT_4:63;
then
A108: y = 0 by A14,A31,FUNCT_2:26;
A109: f.x = b by A106,XTUPLE_0:1;
then f.x in dom G by A98,TARSKI:def 2;
then
A110: F.(f.x) = G.b by A20,A9,A21,A98,A94,A96,A109,FUNCT_4:16
.= 1 by A97,FUNCT_4:63;
F.(f.x) = x by A14,A31,FUNCT_2:26;
hence thesis by A108,A110,ENUMSET1:def 4,NECKLA_2:2;
end;
suppose
A111: [f.x,f.y] = [b,c];
then
A112: f.x = b by XTUPLE_0:1;
then f.x in dom G by A98,TARSKI:def 2;
then F.(f.x) = G.b by A20,A9,A21,A98,A94,A96,A112,FUNCT_4:16
.= 1 by A97,FUNCT_4:63;
then
A113: x = 1 by A14,A31,FUNCT_2:26;
A114: f.y = c by A111,XTUPLE_0:1;
then f.y in dom Hh by A94,TARSKI:def 2;
then
A115: F.(f.y) = Hh.c by A20,A9,A21,A98,A94,A99,A114,FUNCT_4:16
.= 2 by A16,A95,FUNCT_4:63;
F.(f.y) = y by A14,A31,FUNCT_2:26;
hence thesis by A113,A115,ENUMSET1:def 4,NECKLA_2:2;
end;
suppose
A116: [f.x,f.y] = [c,b];
then
A117: f.y = b by XTUPLE_0:1;
then f.y in dom G by A98,TARSKI:def 2;
then F.(f.y) = G.b by A20,A9,A21,A98,A94,A96,A117,FUNCT_4:16
.= 1 by A97,FUNCT_4:63;
then
A118: y = 1 by A14,A31,FUNCT_2:26;
A119: f.x = c by A116,XTUPLE_0:1;
then f.x in dom Hh by A94,TARSKI:def 2;
then
A120: F.(f.x) = Hh.c by A20,A9,A21,A98,A94,A99,A119,FUNCT_4:16
.= 2 by A16,A95,FUNCT_4:63;
F.(f.x) = x by A14,A31,FUNCT_2:26;
hence thesis by A118,A120,ENUMSET1:def 4,NECKLA_2:2;
end;
suppose
A121: [f.x,f.y] = [c,d];
then
A122: f.x = c by XTUPLE_0:1;
then f.x in {c,d} by TARSKI:def 2;
then F.(f.x) = Hh.c by A20,A9,A21,A98,A94,A99,A122,FUNCT_4:16
.= 2 by A16,A95,FUNCT_4:63;
then
A123: x = 2 by A14,A31,FUNCT_2:26;
A124: f.y = d by A121,XTUPLE_0:1;
then f.y in dom Hh by A94,TARSKI:def 2;
then
A125: F.(f.y) = Hh.d by A20,A9,A21,A98,A94,A99,A124,FUNCT_4:16
.= 3 by A95,FUNCT_4:63;
F.(f.y) = y by A14,A31,FUNCT_2:26;
hence thesis by A123,A125,ENUMSET1:def 4,NECKLA_2:2;
end;
suppose
A126: [f.x,f.y] = [d,c];
then
A127: f.y = c by XTUPLE_0:1;
then f.y in {c,d} by TARSKI:def 2;
then F.(f.y) = Hh.c by A20,A9,A21,A98,A94,A99,A127,FUNCT_4:16
.= 2 by A16,A95,FUNCT_4:63;
then
A128: y = 2 by A14,A31,FUNCT_2:26;
A129: f.x = d by A126,XTUPLE_0:1;
then f.x in dom Hh by A94,TARSKI:def 2;
then
A130: F.(f.x) = Hh.d by A20,A9,A21,A98,A94,A99,A129,FUNCT_4:16
.= 3 by A95,FUNCT_4:63;
F.(f.x) = x by A14,A31,FUNCT_2:26;
hence thesis by A128,A130,ENUMSET1:def 4,NECKLA_2:2;
end;
end;
end;
hence thesis by A31;
end;
theorem Th39:
for G being non empty irreflexive symmetric RelStr, x being
Element of G, R1,R2 being non empty RelStr st the carrier of R1 misses the
carrier of R2 & subrelstr ([#]G \ {x}) = union_of(R1,R2) & G is non trivial & G
is path-connected & ComplRelStr G is path-connected holds G embeds Necklace 4
proof
let G be non empty irreflexive symmetric RelStr, x be Element of G, R1,R2 be
non empty RelStr;
assume that
A1: the carrier of R1 misses the carrier of R2 and
A2: subrelstr ([#]G \ {x}) = union_of(R1,R2) and
A3: G is non trivial and
A4: G is path-connected and
A5: ComplRelStr G is path-connected;
consider a being Element of R1 such that
A6: [a,x] in the InternalRel of G by A1,A2,A4,Th37;
set A = (the carrier of G) \ {x}, X = {x};
reconsider A as Subset of G;
set R = subrelstr A;
reconsider R as non empty irreflexive symmetric RelStr by A3,YELLOW_0:def 15;
R = subrelstr ([#]G \ {x}) & R = union_of(R2,R1) by A2,Th8;
then consider b being Element of R2 such that
A7: [b,x] in the InternalRel of G by A1,A4,Th37;
reconsider X1 = {y where y is Element of R1: [y,x] in (the InternalRel of G)
}, Y1 = {y where y is Element of R1: not [y,x] in the InternalRel of G}, X2 = {
y where y is Element of R2: [y,x] in (the InternalRel of G)}, Y2 = {y where y
is Element of R2: not [y,x] in the InternalRel of G} as set;
reconsider X as Subset of G;
set H = subrelstr X;
A8: X1 misses Y1
proof
assume not thesis;
then consider a being object such that
A9: a in X1 & a in Y1 by XBOOLE_0:3;
(ex y1 being Element of R1 st y1 = a & [y1,x] in the InternalRel of G
)& ex y2 being Element of R1 st y2 = a & not [y2,x] in the InternalRel of G by
A9;
hence contradiction;
end;
A10: a in X1 by A6;
A11: the carrier of R1 = X1 \/ Y1
proof
thus the carrier of R1 c= X1 \/ Y1
proof
let a be object;
assume
A12: a in the carrier of R1;
per cases;
suppose
[a,x] in the InternalRel of G;
then a in X1 by A12;
hence thesis by XBOOLE_0:def 3;
end;
suppose
not [a,x] in the InternalRel of G;
then a in Y1 by A12;
hence thesis by XBOOLE_0:def 3;
end;
end;
let a be object such that
A13: a in X1 \/ Y1;
per cases by A13,XBOOLE_0:def 3;
suppose
a in X1;
then ex y being Element of R1 st a = y & [y,x] in (the InternalRel of G);
hence thesis;
end;
suppose
a in Y1;
then ex y being Element of R1 st a = y & not [y,x] in the InternalRel of
G;
hence thesis;
end;
end;
A14: X2 misses Y2
proof
assume not thesis;
then consider a being object such that
A15: a in X2 & a in Y2 by XBOOLE_0:3;
(ex y1 being Element of R2 st y1 = a & [y1,x] in the InternalRel of G
)& ex y2 being Element of R2 st y2 = a & not [y2,x] in the InternalRel of G by
A15;
hence contradiction;
end;
A16: (the carrier of H) misses the carrier of R
proof
assume not thesis;
then (the carrier of H) /\ (the carrier of R) <> {};
then X /\ (the carrier of R) <> {} by YELLOW_0:def 15;
then X /\ A <> {} by YELLOW_0:def 15;
then consider a being object such that
A17: a in X /\ A by XBOOLE_0:def 1;
a in X & a in A by A17,XBOOLE_0:def 4;
hence contradiction by XBOOLE_0:def 5;
end;
reconsider H as non empty irreflexive symmetric RelStr by YELLOW_0:def 15;
A18: b in X2 by A7;
A19: the carrier of G = (the carrier of R) \/ {x}
proof
thus the carrier of G c= (the carrier of R) \/ {x}
proof
let a be object;
assume
A20: a in the carrier of G;
per cases;
suppose
a = x;
then a in {x} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
a <> x;
then not a in {x} by TARSKI:def 1;
then a in (the carrier of G) \ {x} by A20,XBOOLE_0:def 5;
then a in the carrier of R by YELLOW_0:def 15;
hence thesis by XBOOLE_0:def 3;
end;
end;
let a be object;
assume
A21: a in (the carrier of R) \/ {x};
per cases by A21,XBOOLE_0:def 3;
suppose
a in the carrier of R;
then a in (the carrier of G) \ {x} by YELLOW_0:def 15;
hence thesis;
end;
suppose
a in {x};
hence thesis;
end;
end;
A22: the carrier of R2 = X2 \/ Y2
proof
thus the carrier of R2 c= X2 \/ Y2
proof
let a be object;
assume
A23: a in the carrier of R2;
per cases;
suppose
[a,x] in the InternalRel of G;
then a in X2 by A23;
hence thesis by XBOOLE_0:def 3;
end;
suppose
not [a,x] in the InternalRel of G;
then a in Y2 by A23;
hence thesis by XBOOLE_0:def 3;
end;
end;
let a be object such that
A24: a in X2 \/ Y2;
per cases by A24,XBOOLE_0:def 3;
suppose
a in X2;
then ex y being Element of R2 st a = y & [y,x] in (the InternalRel of G);
hence thesis;
end;
suppose
a in Y2;
then ex y being Element of R2 st a = y & not [y,x] in the InternalRel of
G;
hence thesis;
end;
end;
A25: Y1 \/ Y2 is non empty
proof
assume
A26: not thesis;
then
A27: Y2 is empty;
A28: Y1 is empty by A26;
A29: for a being Element of R holds [a,x] in the InternalRel of G
proof
let a be Element of R;
A30: the carrier of R = (the carrier of R1) \/ the carrier of R2 by A2,
NECKLA_2:def 2;
per cases by A30,XBOOLE_0:def 3;
suppose
a in the carrier of R1;
then ex y being Element of R1 st a = y & [y,x] in the InternalRel of G
by A11,A28;
hence thesis;
end;
suppose
a in the carrier of R2;
then ex y being Element of R2 st a = y & [y,x] in the InternalRel of G
by A22,A27;
hence thesis;
end;
end;
not ComplRelStr G is path-connected
proof
A31: a <> x
proof
assume not thesis;
then x in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
then
A32: x in the carrier of R by A2,NECKLA_2:def 2;
x in {x} by TARSKI:def 1;
then x in the carrier of H by YELLOW_0:def 15;
then x in (the carrier of R) /\ the carrier of H by A32,XBOOLE_0:def 4;
hence contradiction by A16;
end;
a in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
then
A33: a in the carrier of R by A2,NECKLA_2:def 2;
the carrier of R c= the carrier of G by A19,XBOOLE_1:7;
then
A34: a is Element of ComplRelStr G by A33,NECKLACE:def 8;
A35: x is Element of ComplRelStr G by NECKLACE:def 8;
assume not thesis;
then (the InternalRel of ComplRelStr G) reduces x,a by A31,A34,A35;
then consider p being FinSequence such that
A36: len p > 0 and
A37: p.1 = x and
A38: p.len p = a and
A39: for i being Nat st i in dom p & i+1 in dom p holds [
p.i, p.(i+1)] in (the InternalRel of ComplRelStr G) by REWRITE1:11;
A40: 0 + 1 <= len p by A36,NAT_1:13;
then len p > 1 by A31,A37,A38,XXREAL_0:1;
then 1+1 <= len p by NAT_1:13;
then
A41: 2 in dom p by FINSEQ_3:25;
1 in dom p by A40,FINSEQ_3:25;
then
A42: [p.1,p.(1+1)] in (the InternalRel of ComplRelStr G) by A39,A41;
A43: p.2 <> x
proof
A44: [x,x] in id the carrier of G by RELAT_1:def 10;
assume not thesis;
then [x,x] in (the InternalRel of ComplRelStr G) /\ id the carrier of
G by A37,A42,A44,XBOOLE_0:def 4;
then (the InternalRel of ComplRelStr G) meets id the carrier of G;
hence contradiction by Th13;
end;
p.2 in the carrier of ComplRelStr G by A42,ZFMISC_1:87;
then
A45: p.2 in the carrier of G by NECKLACE:def 8;
p.2 in the carrier of R
proof
assume not thesis;
then p.2 in {x} by A19,A45,XBOOLE_0:def 3;
hence thesis by A43,TARSKI:def 1;
end;
then
A46: [p.2,x] in the InternalRel of G by A29;
A47: the InternalRel of ComplRelStr G is_symmetric_in the carrier of
ComplRelStr G by NECKLACE:def 3;
p.1 in the carrier of ComplRelStr G & p.(1+1) in the carrier of
ComplRelStr G by A42,ZFMISC_1:87;
then [p.(1+1),p.1] in the InternalRel of ComplRelStr G by A42,A47;
then [p.2,x] in (the InternalRel of ComplRelStr G) /\ the InternalRel
of G by A37,A46,XBOOLE_0:def 4;
then (the InternalRel of ComplRelStr G) meets the InternalRel of G;
hence thesis by Th12;
end;
hence thesis by A5;
end;
thus thesis
proof
per cases by A25;
suppose
A48: Y1 is non empty;
ex b being Element of Y1, c being Element of X1 st [b,c] in the
InternalRel of G
proof
set b = the Element of Y1;
a in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
then
A49: a in the carrier of R by A2,NECKLA_2:def 2;
b in Y1 by A48;
then ex y being Element of R1 st y = b & not [y,x] in the InternalRel
of G;
then b in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
then
A50: b in the carrier of R by A2,NECKLA_2:def 2;
A51: the carrier of R c= the carrier of G by A19,XBOOLE_1:7;
then reconsider a as Element of G by A49;
reconsider b as Element of G by A51,A50;
a <> b
proof
assume
A52: not thesis;
a in X1 by A6;
then a in X1 /\ Y1 by A48,A52,XBOOLE_0:def 4;
hence contradiction by A8;
end;
then (the InternalRel of G) reduces a,b by A4;
then consider p being FinSequence such that
A53: len p > 0 and
A54: p.1 = a and
A55: p.len p = b and
A56: for i being Nat st i in dom p & i+1 in dom p
holds [p.i, p.(i+1)] in (the InternalRel of G) by REWRITE1:11;
defpred P[Nat] means p.$1 in Y1 & $1 in dom p & for k being Nat st k >
$1 holds k in dom p implies p.k in Y1;
for k being Nat st k > len p holds k in dom p implies p.k in Y1
proof
let k be Nat such that
A57: k > len p;
assume k in dom p;
then k in Seg (len p) by FINSEQ_1:def 3;
hence thesis by A57,FINSEQ_1:1;
end;
then P[len p] by A48,A53,A55,CARD_1:27,FINSEQ_5:6;
then
A58: ex k being Nat st P[k];
ex n0 being Nat st P[n0] & for n being Nat st P[n] holds n >= n0
from NAT_1:sch 5(A58);
then consider n0 being Nat such that
A59: P[n0] and
A60: for n being Nat st P[n] holds n >= n0;
n0 <> 0
proof
assume not thesis;
then 0 in Seg (len p) by A59,FINSEQ_1:def 3;
hence contradiction by FINSEQ_1:1;
end;
then consider k0 being Nat such that
A61: n0 = k0 + 1 by NAT_1:6;
A62: n0 <> 1
proof
assume
A63: not thesis;
a in X1 by A6;
then X1 /\ Y1 is non empty by A54,A59,A63,XBOOLE_0:def 4;
hence contradiction by A8;
end;
A64: k0 >= 1
proof
assume not thesis;
then k0 = 0 by NAT_1:25;
hence contradiction by A61,A62;
end;
n0 in Seg (len p) by A59,FINSEQ_1:def 3;
then k0 <= k0 + 1 & n0 <= len p by FINSEQ_1:1,XREAL_1:29;
then
A65: k0 <= len p by A61,XXREAL_0:2;
then
A66: k0 in dom p by A64,FINSEQ_3:25;
then
A67: [p.k0,p.(k0+1)] in the InternalRel of G by A56,A59,A61;
then
A68: the InternalRel of G is_symmetric_in the carrier of G & p.k0 in
the carrier of G by NECKLACE:def 3,ZFMISC_1:87;
p.n0 in the carrier of G by A61,A67,ZFMISC_1:87;
then
A69: [p.n0,p.k0] in the InternalRel of G by A61,A67,A68;
A70: for k being Nat st k > k0 holds k in dom p implies p.k in Y1
proof
assume not thesis;
then consider k being Nat such that
A71: k > k0 and
A72: k in dom p and
A73: not p.k in Y1;
k > n0
proof
per cases by XXREAL_0:1;
suppose
k < n0;
hence thesis by A61,A71,NAT_1:13;
end;
suppose
n0 < k;
hence thesis;
end;
suppose
n0 = k;
hence thesis by A59,A73;
end;
end;
hence contradiction by A59,A72,A73;
end;
k0 < n0 by A61,NAT_1:13;
then
A74: not P[k0] by A60;
p.k0 in the carrier of G by A67,ZFMISC_1:87;
then p.k0 in the carrier of R or p.k0 in {x} by A19,XBOOLE_0:def 3;
then
A75: p.k0 in (the carrier of R1) \/ the carrier of R2 or p.k0 in {x}
by A2,NECKLA_2:def 2;
thus thesis
proof
per cases by A61,A67,A75,XBOOLE_0:def 3,ZFMISC_1:87;
suppose
A76: p.k0 in the carrier of R1 & p.n0 in the carrier of G;
then reconsider
m=p.k0 as Element of X1 by A11,A64,A65,A74,A70,FINSEQ_3:25
,XBOOLE_0:def 3;
m in (the carrier of R1) \/ the carrier of R2 by A76,XBOOLE_0:def 3
;
then
A77: m in the carrier of R by A2,NECKLA_2:def 2;
reconsider l=p.n0 as Element of Y1 by A59;
A78: the carrier of R c= the carrier of G by A19,XBOOLE_1:7;
l in the carrier of R1 by A11,A59,XBOOLE_0:def 3;
then l in (the carrier of R1) \/ the carrier of R2 by
XBOOLE_0:def 3;
then
A79: l in the carrier of R by A2,NECKLA_2:def 2;
[m,l] in the InternalRel of G & the InternalRel of G
is_symmetric_in the carrier of G by A56,A59,A61,A66,NECKLACE:def 3;
then [l,m] in the InternalRel of G by A79,A77,A78;
hence thesis;
end;
suppose
p.k0 in the carrier of R2 & p.n0 in the carrier of G;
then reconsider m=p.k0 as Element of R2;
reconsider l=p.n0 as Element of R1 by A11,A59,XBOOLE_0:def 3;
m in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
then
A80: m in the carrier of R by A2,NECKLA_2:def 2;
l in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
then l in the carrier of R by A2,NECKLA_2:def 2;
then [l,m] in [:the carrier of R,the carrier of R:] by A80,
ZFMISC_1:87;
then [l,m] in (the InternalRel of G)|_2 the carrier of R by A69,
XBOOLE_0:def 4;
then [l,m] in the InternalRel of R by YELLOW_0:def 14;
hence thesis by A1,A2,Th35;
end;
suppose
A81: p.k0 in {x} & p.n0 in the carrier of G;
ex y1 being Element of R1 st p.n0 = y1 & not [y1,x] in the
InternalRel of G by A59;
hence thesis by A69,A81,TARSKI:def 1;
end;
end;
end;
then consider u being Element of Y1, v being Element of X1 such that
A82: [u,v] in the InternalRel of G;
set w = the Element of X2;
w in X2 by A18;
then
A83: ex y being Element of R2 st y = w & [y,x] in the InternalRel of G;
set Z = {u,v,x,w};
Z c= the carrier of G
proof
w in X2 by A18;
then ex y2 being Element of R2 st y2 = w & [y2,x] in the InternalRel
of G;
then w in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
then
A84: w in the carrier of R by A2,NECKLA_2:def 2;
v in X1 by A10;
then ex y1 being Element of R1 st y1 = v & [y1,x] in the InternalRel
of G;
then v in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
then
A85: v in the carrier of R by A2,NECKLA_2:def 2;
u in the carrier of R1 by A11,A48,XBOOLE_0:def 3;
then u in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
then
A86: u in the carrier of R by A2,NECKLA_2:def 2;
let q be object;
assume q in Z;
then
A87: q = u or q = v or q = x or q = w by ENUMSET1:def 2;
the carrier of R c= the carrier of G by A19,XBOOLE_1:7;
hence thesis by A87,A86,A85,A84;
end;
then reconsider Z as Subset of G;
reconsider H = subrelstr Z as non empty full SubRelStr of G by
YELLOW_0:def 15;
A88: w in X2 by A18;
reconsider w as Element of G by A83,ZFMISC_1:87;
A89: v in X1 by A10;
A90: [x,w] in the InternalRel of G
proof
(ex y1 being Element of R2 st w = y1 & [y1,x] in the InternalRel
of G )& the InternalRel of G is_symmetric_in the carrier of G by A88,
NECKLACE:def 3;
hence thesis;
end;
A91: u in Y1 by A48;
reconsider u,v as Element of G by A82,ZFMISC_1:87;
A92: [v,x] in the InternalRel of G
proof
ex y1 being Element of R1 st v = y1 & [y1,x] in the InternalRel
of G by A89;
hence thesis;
end;
A93: w <> u
proof
assume
A94: not thesis;
(ex y1 being Element of R2 st w = y1 & [y1,x] in the InternalRel
of G )& ex y2 being Element of R1 st u = y2 & not [y2,x] in the InternalRel of
G by A91,A88;
hence contradiction by A94;
end;
A95: not [u,x] in the InternalRel of G
proof
ex y1 being Element of R1 st u = y1 & not [y1,x] in the
InternalRel of G by A91;
hence thesis;
end;
A96: not [v,w] in the InternalRel of G
proof
A97: ex y2 being Element of R2 st w = y2 & [y2,x] in the InternalRel
of G by A88;
then w in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
then reconsider w as Element of R by A2,NECKLA_2:def 2;
A98: ex y1 being Element of R1 st v = y1 & [y1,x] in the InternalRel
of G by A89;
then v in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
then reconsider v as Element of R by A2,NECKLA_2:def 2;
assume not thesis;
then [v,w] in (the InternalRel of G)|_2 the carrier of R by
XBOOLE_0:def 4;
then [v,w] in the InternalRel of R by YELLOW_0:def 14;
then
A99: [v,w] in (the InternalRel of R1) \/ (the InternalRel of R2 ) by A2,
NECKLA_2:def 2;
per cases by A99,XBOOLE_0:def 3;
suppose
[v,w] in the InternalRel of R1;
then w in the carrier of R1 by ZFMISC_1:87;
then w in (the carrier of R1) /\ the carrier of R2 by A97,
XBOOLE_0:def 4;
hence contradiction by A1;
end;
suppose
[v,w] in the InternalRel of R2;
then v in the carrier of R2 by ZFMISC_1:87;
then v in (the carrier of R1) /\ the carrier of R2 by A98,
XBOOLE_0:def 4;
hence contradiction by A1;
end;
end;
A100: w <> x
proof
assume
A101: not thesis;
ex y1 being Element of R2 st w = y1 & [y1,x] in the InternalRel
of G by A88;
then x in (the carrier of R1) \/ the carrier of R2 by A101,
XBOOLE_0:def 3;
then x in the carrier of R by A2,NECKLA_2:def 2;
then x in (the carrier of G) \ {x} by YELLOW_0:def 15;
then not x in {x} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1;
end;
A102: not [u,w] in the InternalRel of G
proof
A103: ex y2 being Element of R2 st w = y2 & [y2,x] in the InternalRel
of G by A88;
then w in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
then reconsider w as Element of R by A2,NECKLA_2:def 2;
A104: ex y1 being Element of R1 st u = y1 & not [y1,x] in the
InternalRel of G by A91;
then u in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
then reconsider u as Element of R by A2,NECKLA_2:def 2;
assume not thesis;
then [u,w] in (the InternalRel of G)|_2 the carrier of R by
XBOOLE_0:def 4;
then [u,w] in the InternalRel of R by YELLOW_0:def 14;
then
A105: [u,w] in (the InternalRel of R1) \/ (the InternalRel of R2 ) by A2,
NECKLA_2:def 2;
per cases by A105,XBOOLE_0:def 3;
suppose
[u,w] in the InternalRel of R1;
then w in the carrier of R1 by ZFMISC_1:87;
then w in (the carrier of R1) /\ the carrier of R2 by A103,
XBOOLE_0:def 4;
hence contradiction by A1;
end;
suppose
[u,w] in the InternalRel of R2;
then u in the carrier of R2 by ZFMISC_1:87;
then u in (the carrier of R1) /\ the carrier of R2 by A104,
XBOOLE_0:def 4;
hence contradiction by A1;
end;
end;
A106: x <> u
proof
assume
A107: not thesis;
ex y1 being Element of R1 st u = y1 & not [y1,x] in the
InternalRel of G by A91;
then x in (the carrier of R1) \/ (the carrier of R2) by A107,
XBOOLE_0:def 3;
then x in the carrier of R by A2,NECKLA_2:def 2;
then x in (the carrier of G) \ {x} by YELLOW_0:def 15;
then not x in {x} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1;
end;
A108: w <> v
proof
consider y1 being Element of R2 such that
A109: w = y1 and
[y1,x] in the InternalRel of G by A88;
assume
A110: not thesis;
ex y2 being Element of R1 st v = y2 & [y2,x] in the InternalRel
of G by A89;
then y1 in (the carrier of R1) /\ (the carrier of R2) by A110,A109,
XBOOLE_0:def 4;
hence contradiction by A1;
end;
A111: v <> x
proof
assume
A112: not thesis;
ex y1 being Element of R1 st v = y1 & [y1,x] in the InternalRel
of G by A89;
then x in (the carrier of R1) \/ the carrier of R2 by A112,
XBOOLE_0:def 3;
then x in the carrier of R by A2,NECKLA_2:def 2;
then x in (the carrier of G) \ {x} by YELLOW_0:def 15;
then not x in {x} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1;
end;
u <> v
proof
assume
A113: not thesis;
(ex y1 being Element of R1 st u = y1 & not [y1,x] in the
InternalRel of G )& ex y2 being Element of R1 st v = y2 & [y2,x] in the
InternalRel of G by A91,A89;
hence contradiction by A113;
end;
then u,v,x,w are_mutually_distinct by A111,A106,A93,A108,A100,
ZFMISC_1:def 6;
then
A114: subrelstr Z embeds Necklace 4 by A82,A92,A90,A95,A102,A96,Th38;
G embeds Necklace 4
proof
assume not thesis;
then G is N-free by NECKLA_2:def 1;
then H is N-free by Th23;
hence thesis by A114,NECKLA_2:def 1;
end;
hence thesis;
end;
suppose
A115: Y2 is non empty;
ex c being Element of Y2, d being Element of X2 st [c,d] in the
InternalRel of G
proof
set c = the Element of Y2;
b in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
then
A116: b in the carrier of R by A2,NECKLA_2:def 2;
c in Y2 by A115;
then ex y being Element of R2 st y = c & not [y,x] in the InternalRel
of G;
then c in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
then
A117: c in the carrier of R by A2,NECKLA_2:def 2;
A118: the carrier of R c= the carrier of G by A19,XBOOLE_1:7;
then reconsider b as Element of G by A116;
reconsider c as Element of G by A118,A117;
b <> c
proof
assume not thesis;
then c in X2 by A7;
then c in X2 /\ Y2 by A115,XBOOLE_0:def 4;
hence contradiction by A14;
end;
then (the InternalRel of G) reduces b,c by A4;
then consider p being FinSequence such that
A119: len p > 0 and
A120: p.1 = b and
A121: p.len p = c and
A122: for i being Nat st i in dom p & i+1 in dom p
holds [p.i, p.(i+1)] in (the InternalRel of G) by REWRITE1:11;
defpred P[Nat] means p.$1 in Y2 & $1 in dom p & for k being Nat st k >
$1 holds k in dom p implies p.k in Y2;
for k being Nat st k > len p holds k in dom p implies p.k in Y2
proof
let k be Nat such that
A123: k > len p;
assume k in dom p;
then k in Seg (len p) by FINSEQ_1:def 3;
hence thesis by A123,FINSEQ_1:1;
end;
then P[len p] by A115,A119,A121,CARD_1:27,FINSEQ_5:6;
then
A124: ex k being Nat st P[k];
ex n0 being Nat st P[n0] & for n being Nat st P[n] holds n >= n0
from NAT_1:sch 5(A124);
then consider n0 being Nat such that
A125: P[n0] and
A126: for n being Nat st P[n] holds n >= n0;
n0 <> 0
proof
assume not thesis;
then 0 in Seg (len p) by A125,FINSEQ_1:def 3;
hence contradiction by FINSEQ_1:1;
end;
then consider k0 being Nat such that
A127: n0 = k0 + 1 by NAT_1:6;
A128: n0 <> 1
proof
assume
A129: not thesis;
b in X2 by A7;
then X2 /\ Y2 is non empty by A120,A125,A129,XBOOLE_0:def 4;
hence contradiction by A14;
end;
A130: k0 >= 1
proof
assume not thesis;
then k0 = 0 by NAT_1:25;
hence contradiction by A127,A128;
end;
n0 in Seg (len p) by A125,FINSEQ_1:def 3;
then k0 <= k0 + 1 & n0 <= len p by FINSEQ_1:1,XREAL_1:29;
then k0 <= len p by A127,XXREAL_0:2;
then
A131: k0 in Seg (len p) by A130,FINSEQ_1:1;
then
A132: k0 in dom p by FINSEQ_1:def 3;
then
A133: [p.k0,p.(k0+1)] in the InternalRel of G by A122,A125,A127;
then
A134: the InternalRel of G is_symmetric_in the carrier of G & p.k0 in
the carrier of G by NECKLACE:def 3,ZFMISC_1:87;
p.n0 in the carrier of G by A127,A133,ZFMISC_1:87;
then
A135: [p.n0,p.k0] in the InternalRel of G by A127,A133,A134;
A136: for k being Nat st k > k0 holds k in dom p implies p.k in Y2
proof
assume not thesis;
then consider k being Nat such that
A137: k > k0 and
A138: k in dom p and
A139: not p.k in Y2;
k > n0
proof
per cases by XXREAL_0:1;
suppose
k < n0;
hence thesis by A127,A137,NAT_1:13;
end;
suppose
n0 < k;
hence thesis;
end;
suppose
n0 = k;
hence thesis by A125,A139;
end;
end;
hence contradiction by A125,A138,A139;
end;
k0 < n0 by A127,NAT_1:13;
then
A140: not P[k0] by A126;
p.k0 in the carrier of G by A133,ZFMISC_1:87;
then p.k0 in the carrier of R or p.k0 in {x} by A19,XBOOLE_0:def 3;
then
A141: p.k0 in (the carrier of R1) \/ the carrier of R2 or p.k0 in {x}
by A2,NECKLA_2:def 2;
thus thesis
proof
per cases by A127,A133,A141,XBOOLE_0:def 3,ZFMISC_1:87;
suppose
p.k0 in the carrier of R2 & p.n0 in the carrier of G;
then reconsider m=p.k0 as Element of X2 by A22,A131,A140,A136,
FINSEQ_1:def 3,XBOOLE_0:def 3;
reconsider l=p.n0 as Element of Y2 by A125;
[m,l] in the InternalRel of G by A122,A125,A127,A132;
hence thesis by A135;
end;
suppose
p.k0 in the carrier of R1 & p.n0 in the carrier of G;
then reconsider m=p.k0 as Element of R1;
reconsider l=p.n0 as Element of R2 by A22,A125,XBOOLE_0:def 3;
A142: the InternalRel of R is_symmetric_in the carrier of R by
NECKLACE:def 3;
m in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
then
A143: m in the carrier of R by A2,NECKLA_2:def 2;
l in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
then
A144: l in the carrier of R by A2,NECKLA_2:def 2;
then [l,m] in [:the carrier of R,the carrier of R:] by A143,
ZFMISC_1:87;
then [l,m] in (the InternalRel of G)|_2 the carrier of R by A135,
XBOOLE_0:def 4;
then [l,m] in the InternalRel of R by YELLOW_0:def 14;
then [m,l] in the InternalRel of R by A144,A143,A142;
hence thesis by A1,A2,Th35;
end;
suppose
A145: p.k0 in {x} & p.n0 in the carrier of G;
ex y1 being Element of R2 st p.n0 = y1 & not [y1,x] in the
InternalRel of G by A125;
hence thesis by A135,A145,TARSKI:def 1;
end;
end;
end;
then consider u being Element of Y2, v being Element of X2 such that
A146: [u,v] in the InternalRel of G;
set w = the Element of X1;
w in X1 by A10;
then
A147: ex y being Element of R1 st y = w & [y,x] in the InternalRel of G;
set Z = {u,v,x,w};
Z c= the carrier of G
proof
w in X1 by A10;
then ex y2 being Element of R1 st y2 = w & [y2,x] in the InternalRel
of G;
then w in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
then
A148: w in the carrier of R by A2,NECKLA_2:def 2;
v in X2 by A18;
then ex y1 being Element of R2 st y1 = v & [y1,x] in the InternalRel
of G;
then v in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
then
A149: v in the carrier of R by A2,NECKLA_2:def 2;
u in the carrier of R2 by A22,A115,XBOOLE_0:def 3;
then u in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
then
A150: u in the carrier of R by A2,NECKLA_2:def 2;
let q be object;
assume q in Z;
then
A151: q = u or q = v or q = x or q = w by ENUMSET1:def 2;
the carrier of R c= the carrier of G by A19,XBOOLE_1:7;
hence thesis by A151,A150,A149,A148;
end;
then reconsider Z as Subset of G;
reconsider H = subrelstr Z as non empty full SubRelStr of G by
YELLOW_0:def 15;
A152: w in X1 by A10;
reconsider w as Element of G by A147,ZFMISC_1:87;
A153: v in X2 by A18;
A154: [x,w] in the InternalRel of G
proof
(ex y1 being Element of R1 st w = y1 & [y1,x] in the InternalRel
of G )& the InternalRel of G is_symmetric_in the carrier of G by A152,
NECKLACE:def 3;
hence thesis;
end;
A155: u in Y2 by A115;
reconsider u,v as Element of G by A146,ZFMISC_1:87;
A156: [v,x] in the InternalRel of G
proof
ex y1 being Element of R2 st v = y1 & [y1,x] in the InternalRel
of G by A153;
hence thesis;
end;
A157: w <> u
proof
assume
A158: not thesis;
(ex y1 being Element of R1 st w = y1 & [y1,x] in the InternalRel
of G )& ex y2 being Element of R2 st u = y2 & not [y2,x] in the InternalRel of
G by A155,A152;
hence contradiction by A158;
end;
A159: not [u,x] in the InternalRel of G
proof
ex y1 being Element of R2 st u = y1 & not [y1,x] in the
InternalRel of G by A155;
hence thesis;
end;
A160: not [v,w] in the InternalRel of G
proof
A161: ex y2 being Element of R1 st w = y2 & [y2,x] in the InternalRel
of G by A152;
then w in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
then reconsider w as Element of R by A2,NECKLA_2:def 2;
A162: ex y1 being Element of R2 st v = y1 & [y1,x] in the InternalRel
of G by A153;
then v in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
then reconsider v as Element of R by A2,NECKLA_2:def 2;
assume not thesis;
then [v,w] in (the InternalRel of G)|_2 the carrier of R by
XBOOLE_0:def 4;
then [v,w] in the InternalRel of R by YELLOW_0:def 14;
then
A163: [v,w] in (the InternalRel of R1) \/ (the InternalRel of R2 ) by A2,
NECKLA_2:def 2;
per cases by A163,XBOOLE_0:def 3;
suppose
[v,w] in the InternalRel of R1;
then v in the carrier of R1 by ZFMISC_1:87;
then v in (the carrier of R1) /\ the carrier of R2 by A162,
XBOOLE_0:def 4;
hence contradiction by A1;
end;
suppose
[v,w] in the InternalRel of R2;
then w in the carrier of R2 by ZFMISC_1:87;
then w in (the carrier of R1) /\ the carrier of R2 by A161,
XBOOLE_0:def 4;
hence contradiction by A1;
end;
end;
A164: w <> x
proof
assume
A165: not thesis;
ex y1 being Element of R1 st w = y1 & [y1,x] in the InternalRel
of G by A152;
then x in (the carrier of R1) \/ the carrier of R2 by A165,
XBOOLE_0:def 3;
then x in the carrier of R by A2,NECKLA_2:def 2;
then x in (the carrier of G) \ {x} by YELLOW_0:def 15;
then not x in {x} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1;
end;
A166: not [u,w] in the InternalRel of G
proof
A167: ex y2 being Element of R1 st w = y2 & [y2,x] in the InternalRel
of G by A152;
then w in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
then reconsider w as Element of R by A2,NECKLA_2:def 2;
A168: ex y1 being Element of R2 st u = y1 & not [y1,x] in the
InternalRel of G by A155;
then u in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
then reconsider u as Element of R by A2,NECKLA_2:def 2;
assume not thesis;
then [u,w] in (the InternalRel of G)|_2 the carrier of R by
XBOOLE_0:def 4;
then [u,w] in the InternalRel of R by YELLOW_0:def 14;
then
A169: [u,w] in (the InternalRel of R1) \/ (the InternalRel of R2 ) by A2,
NECKLA_2:def 2;
per cases by A169,XBOOLE_0:def 3;
suppose
[u,w] in the InternalRel of R1;
then u in the carrier of R1 by ZFMISC_1:87;
then u in (the carrier of R1) /\ the carrier of R2 by A168,
XBOOLE_0:def 4;
hence contradiction by A1;
end;
suppose
[u,w] in the InternalRel of R2;
then w in the carrier of R2 by ZFMISC_1:87;
then w in (the carrier of R1) /\ the carrier of R2 by A167,
XBOOLE_0:def 4;
hence contradiction by A1;
end;
end;
A170: x <> u
proof
assume
A171: not thesis;
ex y1 being Element of R2 st u = y1 & not [y1,x] in the
InternalRel of G by A155;
then x in (the carrier of R1) \/ (the carrier of R2) by A171,
XBOOLE_0:def 3;
then x in the carrier of R by A2,NECKLA_2:def 2;
then x in (the carrier of G) \ {x} by YELLOW_0:def 15;
then not x in {x} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1;
end;
A172: w <> v
proof
consider y1 being Element of R1 such that
A173: w = y1 and
[y1,x] in the InternalRel of G by A152;
assume
A174: not thesis;
ex y2 being Element of R2 st v = y2 & [y2,x] in the InternalRel
of G by A153;
then y1 in (the carrier of R1) /\ (the carrier of R2) by A174,A173,
XBOOLE_0:def 4;
hence contradiction by A1;
end;
A175: v <> x
proof
assume
A176: not thesis;
ex y1 being Element of R2 st v = y1 & [y1,x] in the InternalRel
of G by A153;
then x in (the carrier of R1) \/ the carrier of R2 by A176,
XBOOLE_0:def 3;
then x in the carrier of R by A2,NECKLA_2:def 2;
then x in (the carrier of G) \ {x} by YELLOW_0:def 15;
then not x in {x} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1;
end;
u <> v
proof
assume
A177: not thesis;
(ex y1 being Element of R2 st u = y1 & not [y1,x] in the
InternalRel of G )& ex y2 being Element of R2 st v = y2 & [y2,x] in the
InternalRel of G by A155,A153;
hence contradiction by A177;
end;
then u,v,x,w are_mutually_distinct by A175,A170,A157,A172,A164,
ZFMISC_1:def 6;
then
A178: subrelstr Z embeds Necklace 4 by A146,A156,A154,A159,A166,A160,Th38;
G embeds Necklace 4
proof
assume not thesis;
then G is N-free by NECKLA_2:def 1;
then H is N-free by Th23;
hence thesis by A178,NECKLA_2:def 1;
end;
hence thesis;
end;
end;
end;
theorem
for G being non empty strict finite irreflexive symmetric RelStr st G
is N-free & the carrier of G in FinSETS holds the RelStr of G in fin_RelStr_sp
proof
let R be non empty strict finite irreflexive symmetric RelStr;
defpred P[Nat] means for G be non empty strict finite irreflexive symmetric
RelStr st G is N-free & card the carrier of G = $1 & the carrier of G in
FinSETS holds (the RelStr of G) in fin_RelStr_sp;
A1: for n be Nat st for k be Nat st k < n holds P[k] holds P[n]
proof
let n be Nat such that
A2: for k be Nat st k < n holds P[k];
let G be non empty strict finite irreflexive symmetric RelStr;
set CG = ComplRelStr G;
assume that
A3: G is N-free and
A4: card (the carrier of G) = n and
A5: (the carrier of G) in FinSETS;
per cases;
suppose
G is trivial;
then the carrier of G is 1-element;
then reconsider G as 1-element RelStr by STRUCT_0:def 19;
(the RelStr of G) in fin_RelStr_sp by A5,NECKLA_2:def 5;
hence thesis;
end;
suppose
G is not path-connected & G is non trivial;
then consider
G1,G2 being non empty strict irreflexive symmetric RelStr such
that
A6: (the carrier of G1) misses (the carrier of G2) and
A7: the RelStr of G = union_of(G1,G2) by Th30;
set cG1 = the carrier of G1, cG2 = the carrier of G2, R = the RelStr of
G, cR = the carrier of R;
reconsider cR as finite set;
A8: cR = cG1 \/ cG2 by A7,NECKLA_2:def 2;
then
A9: card cG1 in Segm card cR by A6,Lm1;
then reconsider
G1 as non empty strict finite irreflexive symmetric RelStr;
reconsider cR as finite set;
A10: card cG2 in Segm card cR by A6,A8,Lm1;
then reconsider
G2 as non empty strict finite irreflexive symmetric RelStr;
reconsider cG2 as finite set by A10;
A11: card cG2 < card cR by A10,NAT_1:44;
G2 is full SubRelStr of G by A6,A7,Th10;
then
A12: G2 is N-free by A3,Th23;
the carrier of G2 in FinSETS by A5,A8,CLASSES1:3,CLASSES2:def 2
,XBOOLE_1:7;
then
A13: G2 in fin_RelStr_sp by A2,A4,A11,A12;
G1 is full SubRelStr of G by A6,A7,Th10;
then
A14: G1 is N-free by A3,Th23;
reconsider cG1 as finite set by A9;
A15: card cG1 < card cR by A9,NAT_1:44;
the carrier of G1 in FinSETS by A5,A8,CLASSES1:3,CLASSES2:def 2
,XBOOLE_1:7;
then G1 in fin_RelStr_sp by A2,A4,A15,A14;
hence thesis by A6,A7,A13,NECKLA_2:def 5;
end;
suppose
CG is not path-connected & G is non trivial;
then consider
G1,G2 being non empty strict irreflexive symmetric RelStr such
that
A16: (the carrier of G1) misses (the carrier of G2) and
A17: (the RelStr of G) = sum_of(G1,G2) by Th31;
set cG1 = the carrier of G1, cG2 = the carrier of G2, R = the RelStr of
G, cR = the carrier of R;
reconsider cR as finite set;
A18: cR = cG1 \/ cG2 by A17,NECKLA_2:def 3;
then
A19: card cG1 in Segm card cR by A16,Lm1;
then reconsider
G1 as non empty strict finite irreflexive symmetric RelStr;
A20: card cG2 in Segm card cR by A16,A18,Lm1;
then reconsider
G2 as non empty strict finite irreflexive symmetric RelStr;
reconsider cG2 as finite set by A20;
A21: card cG2 < card cR by A20,NAT_1:44;
G2 is full SubRelStr of G by A16,A17,Th10;
then
A22: G2 is N-free by A3,Th23;
the carrier of G2 in FinSETS by A5,A18,CLASSES1:3,CLASSES2:def 2
,XBOOLE_1:7;
then
A23: G2 in fin_RelStr_sp by A2,A4,A21,A22;
G1 is full SubRelStr of G by A16,A17,Th10;
then
A24: G1 is N-free by A3,Th23;
reconsider cG1 as finite set by A19;
A25: card cG1 < card cR by A19,NAT_1:44;
the carrier of G1 in FinSETS by A5,A18,CLASSES1:3,CLASSES2:def 2
,XBOOLE_1:7;
then G1 in fin_RelStr_sp by A2,A4,A25,A24;
hence thesis by A16,A17,A23,NECKLA_2:def 5;
end;
suppose
A26: G is non trivial & G is path-connected & CG is path-connected;
consider x be object such that
A27: x in the carrier of G by XBOOLE_0:def 1;
reconsider x as Element of G by A27;
set A = (the carrier of G) \ {x};
A28: A c= the carrier of G;
reconsider A as Subset of G;
set R = subrelstr A;
reconsider R as non empty finite irreflexive symmetric RelStr by A26,
YELLOW_0:def 15;
A29: the carrier of R c= the carrier of G by A28,YELLOW_0:def 15;
card A = card (the carrier of G) - card {x} by CARD_2:44;
then
A30: card A = n - 1 by A4,CARD_2:42;
n - 1 < n - 1 + 1 by XREAL_1:29;
then
A31: card the carrier of R < n by A30,YELLOW_0:def 15;
R is N-free by A3,Th23;
then
A32: R in fin_RelStr_sp by A2,A5,A31,A29,CLASSES1:3,CLASSES2:def 2;
thus thesis
proof
per cases by A32,NECKLA_2:6;
suppose
A33: R is trivial RelStr;
the carrier of R is non empty;
then
A34: A is non empty by YELLOW_0:def 15;
A is trivial by A33,YELLOW_0:def 15;
then consider a be object such that
A35: A = {a} by A34,ZFMISC_1:131;
A36: (the carrier of G) \/ {x} = the carrier of G
proof
thus (the carrier of G) \/ {x} c= the carrier of G
proof
let c be object;
assume c in (the carrier of G) \/ {x};
then c in the carrier of G or c in {x} by XBOOLE_0:def 3;
hence thesis;
end;
let c be object;
assume c in the carrier of G;
hence thesis by XBOOLE_0:def 3;
end;
{a} \/ {x} = (the carrier of G) \/ {x} by A35,XBOOLE_1:39;
then the carrier of G = {a,x} & a <> x by A26,A36,ENUMSET1:1;
then card (the carrier of G) = 2 by CARD_2:57;
hence thesis by A5,Th33;
end;
suppose
ex R1,R2 being strict RelStr st (the carrier of R1) misses
(the carrier of R2) & R1 in fin_RelStr_sp & R2 in fin_RelStr_sp & (R = union_of
(R1,R2) or R = sum_of(R1,R2) );
then consider R1,R2 being strict RelStr such that
A37: (the carrier of R1) misses (the carrier of R2) and
A38: R1 in fin_RelStr_sp and
A39: R2 in fin_RelStr_sp and
A40: R = union_of(R1,R2) or R = sum_of(R1,R2);
thus thesis
proof
per cases by A40;
suppose
A41: R = union_of(R1,R2);
R2 is SubRelStr of R by A37,A40,Th10;
then reconsider R2 as non empty SubRelStr of G by A39,NECKLA_2:4
,YELLOW_6:7;
R1 is SubRelStr of R by A37,A40,Th10;
then reconsider R1 as non empty SubRelStr of G by A38,NECKLA_2:4
,YELLOW_6:7;
subrelstr ([#]G \ {x}) = union_of(R1,R2) by A41;
then G embeds Necklace 4 by A26,A37,Th39;
hence thesis by A3,NECKLA_2:def 1;
end;
suppose
A42: R = sum_of(R1,R2);
ComplRelStr R2 is non empty
proof
assume not thesis;
then R2 is empty;
hence contradiction by A39,NECKLA_2:4;
end;
then reconsider R22 = ComplRelStr R2 as non empty RelStr;
ComplRelStr R1 is non empty
proof
assume not thesis;
then R1 is empty;
hence contradiction by A38,NECKLA_2:4;
end;
then reconsider R11 = ComplRelStr R1 as non empty RelStr;
reconsider G9 = ComplRelStr G as non empty irreflexive symmetric
RelStr;
reconsider x9 = x as Element of G9 by NECKLACE:def 8;
A43: the carrier of R11 = the carrier of R1 & the carrier of R22
= the carrier of R2 by NECKLACE:def 8;
A44: ComplRelStr R = ComplRelStr (subrelstr ([#]G \ {x}))
.= subrelstr ([#](G9) \ {x9}) by Th20;
A45: G9 is N-free by A3,Th25;
A46: ComplRelStr G9 is path-connected & G9 is non trivial by A26,Th16,
NECKLACE:def 8;
ComplRelStr R = union_of(ComplRelStr R1, ComplRelStr R2) by A37
,A42,Th18;
then G9 embeds Necklace 4 by A26,A37,A43,A46,A44,Th39;
hence thesis by A45,NECKLA_2:def 1;
end;
end;
end;
end;
end;
end;
A47: for k be Nat holds P[k] from NAT_1:sch 4(A1);
card the carrier of R is Nat;
hence thesis by A47;
end;