:: Properties of Binary Relations
:: by Edmund Woronowicz and Anna Zalewska
::
:: Received March 15, 1989
:: Copyright (c) 1990-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 RELAT_1, TARSKI, XBOOLE_0, ZFMISC_1, RELAT_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1;
constructors TARSKI, SUBSET_1, RELAT_1, XTUPLE_0;
registrations RELAT_1, XBOOLE_0;
requirements BOOLE, SUBSET;
definitions RELAT_1;
equalities RELAT_1;
expansions RELAT_1;
theorems TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, XTUPLE_0;
begin
reserve X for set, a,b,c,x,y,z for object;
reserve P,R for Relation;
definition
let R,X;
pred R is_reflexive_in X means
:Def1:
x in X implies [x,x] in R;
pred R is_irreflexive_in X means
:Def2:
x in X implies not [x,x] in R;
pred R is_symmetric_in X means
:Def3:
x in X & y in X & [x,y] in R implies [ y,x] in R;
pred R is_antisymmetric_in X means
:Def4:
x in X & y in X & [x,y] in R & [y, x] in R implies x = y;
pred R is_asymmetric_in X means
x in X & y in X & [x,y] in R implies not [y,x] in R;
pred R is_connected_in X means
:Def6:
x in X & y in X & x <>y implies [x,y] in R or [y,x] in R;
pred R is_strongly_connected_in X means
:Def7:
x in X & y in X implies [x,y] in R or [y,x] in R;
pred R is_transitive_in X means
:Def8:
x in X & y in X & z in X & [x,y] in R & [y,z] in R implies [x,z] in R;
end;
definition
let R;
attr R is reflexive means
:Def9:
R is_reflexive_in field R;
attr R is irreflexive means
:Def10:
R is_irreflexive_in field R;
attr R is symmetric means
:Def11:
R is_symmetric_in field R;
attr R is antisymmetric means
:Def12:
R is_antisymmetric_in field R;
attr R is asymmetric means
:Def13:
R is_asymmetric_in field R;
attr R is connected means
R is_connected_in field R;
attr R is strongly_connected means
R is_strongly_connected_in field R;
attr R is transitive means
:Def16:
R is_transitive_in field R;
end;
registration
cluster empty -> reflexive irreflexive symmetric antisymmetric asymmetric
connected strongly_connected transitive for Relation;
coherence
proof
let R be Relation;
assume
A1: R is empty;
thus R is reflexive
proof
let x;
thus thesis by A1,RELAT_1:40;
end;
thus R is irreflexive
proof
let x;
thus thesis by A1;
end;
thus R is symmetric
proof
let x;
thus thesis by A1;
end;
thus R is antisymmetric
proof
let x;
thus thesis by A1;
end;
thus R is asymmetric
proof
let x;
thus thesis by A1;
end;
thus R is connected
proof
let x;
thus thesis by A1,RELAT_1:40;
end;
thus R is strongly_connected
proof
let x;
thus thesis by A1,RELAT_1:40;
end;
let x;
thus thesis by A1;
end;
end;
theorem
R is reflexive iff id field R c= R
proof
hereby
assume
A1: R is reflexive;
thus id field R c= R
proof
let a,b be object;
assume [a,b] in id field R;
then a in field R & a = b by RELAT_1:def 10;
hence [a,b] in R by A1,Def1;
end;
end;
assume
A2: id field R c= R;
let a;
assume a in field R;
then [a,a] in id field R by RELAT_1:def 10;
hence [a,a] in R by A2;
end;
theorem
R is irreflexive iff id field R misses R
proof
hereby
assume R is irreflexive;
then
A1: R is_irreflexive_in field R;
now
let a,b be object;
assume
A2: [a,b] in id (field R) /\ R;
then [a,b] in id (field R) by XBOOLE_0:def 4;
then
A3: a in field R & a = b by RELAT_1:def 10;
[a,b] in R by A2,XBOOLE_0:def 4;
hence contradiction by A1,A3;
end;
hence id (field R) misses R by RELAT_1:37,XBOOLE_0:def 7;
end;
assume
A4: id (field R) misses R;
let a;
assume a in field R;
then [a,a] in id field R by RELAT_1:def 10;
hence thesis by A4,XBOOLE_0:3;
end;
theorem
R is_antisymmetric_in X iff R \ id X is_asymmetric_in X
proof
hereby
assume
A1: R is_antisymmetric_in X;
thus R \ id X is_asymmetric_in X
proof
let x,y;
assume that
A2: x in X and
A3: y in X and
A4: [x,y] in R \ id X;
not [x,y] in id X by A4,XBOOLE_0:def 5;
then
A5: x <> y by A2,RELAT_1:def 10;
[x,y] in R by A4,XBOOLE_0:def 5;
then not [y,x] in R by A1,A2,A3,A5;
hence not [y,x] in R \ id X by XBOOLE_0:def 5;
end;
end;
assume
A6: R \ id X is_asymmetric_in X;
let x,y;
assume that
A7: x in X & y in X and
A8: [x,y] in R and
A9: [y,x] in R;
assume
A10: x <> y;
then not [y,x] in id X by RELAT_1:def 10;
then
A11: [y,x] in R \ id X by A9,XBOOLE_0:def 5;
not [x,y] in id X by A10,RELAT_1:def 10;
then [x,y] in R \ id X by A8,XBOOLE_0:def 5;
hence contradiction by A6,A7,A11;
end;
theorem
R is_asymmetric_in X implies R \/ id X is_antisymmetric_in X
proof
assume
A1: R is_asymmetric_in X;
let x,y;
assume that
A2: x in X & y in X and
A3: [x,y] in R \/ id X and
A4: [y,x] in R \/ id X;
assume
A5: x <> y;
then not [y,x] in id X by RELAT_1:def 10;
then
A6: [y,x] in R by A4,XBOOLE_0:def 3;
not [x,y] in id X by A5,RELAT_1:def 10;
then [x,y] in R by A3,XBOOLE_0:def 3;
hence contradiction by A1,A2,A6;
end;
::$CT 7
registration
cluster symmetric transitive -> reflexive for Relation;
coherence
proof
let R be Relation;
assume that
A1: R is symmetric and
A2: R is transitive;
A3: R is_transitive_in field R by A2;
A4: R is_symmetric_in field R by A1;
let a;
A5: now
assume a in dom R;
then consider b being object such that
A6: [a,b] in R by XTUPLE_0:def 12;
A7: a in field R & b in field R by A6,RELAT_1:15;
then [b,a] in R by A4,A6;
hence [a,a] in R by A3,A6,A7;
end;
now
assume a in rng R;
then consider b being object such that
A8: [b,a] in R by XTUPLE_0:def 13;
A9: a in field R & b in field R by A8,RELAT_1:15;
then [a,b] in R by A4,A8;
hence [a,a] in R by A3,A8,A9;
end;
hence thesis by A5,XBOOLE_0:def 3;
end;
end;
registration
let X;
cluster id X -> symmetric transitive antisymmetric;
coherence
proof
thus id X is symmetric
proof
let a,b;
assume that
a in field(id X) and
b in field(id X) and
A1: [a,b] in id X;
a = b by A1,RELAT_1:def 10;
hence thesis by A1;
end;
thus id X is transitive
proof
let a,b,c;
thus thesis by RELAT_1:def 10;
end;
thus id X is antisymmetric
proof
let a,b;
thus thesis by RELAT_1:def 10;
end;
end;
end;
registration
cluster irreflexive transitive -> asymmetric for Relation;
coherence
proof
let R be Relation;
assume that
A1: R is_irreflexive_in field R and
A2: R is_transitive_in field R;
let a,b;
assume that
A3: a in field R and
A4: b in field R;
not [a,a] in R by A1,A3;
hence thesis by A2,A3,A4;
end;
cluster asymmetric -> irreflexive antisymmetric for Relation;
coherence
proof
let R be Relation;
assume
A5: R is_asymmetric_in field R;
then for x holds x in field R implies not [x,x] in R;
hence R is irreflexive by Def2;
for x,y holds x in field R & y in field R & [x,y] in R & [y,x] in R
implies x = y by A5;
hence thesis by Def4;
end;
end;
registration
let R be reflexive Relation;
cluster R~ -> reflexive;
coherence
proof
A1: R is_reflexive_in field R by Def9;
let x;
assume x in field(R~);
then x in field R by RELAT_1:21;
then [x,x] in R by A1;
hence [x,x] in R~ by RELAT_1:def 7;
end;
end;
registration
let R be irreflexive Relation;
cluster R~ -> irreflexive;
coherence
proof
A1: R is_irreflexive_in field R by Def10;
let x;
assume x in field(R~);
then x in field R by RELAT_1:21;
then not [x,x] in R by A1;
hence thesis by RELAT_1:def 7;
end;
end;
theorem
R is reflexive implies dom R = dom(R~) & rng R = rng(R~)
proof
assume
A1: R is reflexive; then
A2: R is_reflexive_in field R;
A3: R~ is_reflexive_in field(R~) by A1,Def9;
now
let x be object;
A4: now
assume x in dom(R~);
then x in field(R~) by XBOOLE_0:def 3;
then [x,x] in R~ by A1,Def1,Def9;
then [x,x] in R by RELAT_1:def 7;
hence x in dom R by XTUPLE_0:def 12;
end;
now
assume x in dom R;
then x in field R by XBOOLE_0:def 3;
then [x,x] in R by A1,Def1;
then [x,x] in R~ by RELAT_1:def 7;
hence x in dom(R~) by XTUPLE_0:def 12;
end;
hence x in dom R iff x in dom(R~) by A4;
end;
hence dom R = dom(R~) by TARSKI:2;
now
let x be object;
A5: now
assume x in rng(R~);
then x in field(R~) by XBOOLE_0:def 3;
then [x,x] in R~ by A3;
then [x,x] in R by RELAT_1:def 7;
hence x in rng R by XTUPLE_0:def 13;
end;
now
assume x in rng R;
then x in field R by XBOOLE_0:def 3;
then [x,x] in R by A2;
then [x,x] in R~ by RELAT_1:def 7;
hence x in rng(R~) by XTUPLE_0:def 13;
end;
hence x in rng R iff x in rng(R~) by A5;
end;
hence thesis by TARSKI:2;
end;
theorem Th6:
R is symmetric iff R = R~
proof
hereby
assume R is symmetric;
then
A1: R is_symmetric_in field R;
now
let a,b be object;
A2: now
assume [a,b] in R~;
then
A3: [b,a] in R by RELAT_1:def 7;
then a in field R & b in field R by RELAT_1:15;
hence [a,b] in R by A1,A3;
end;
now
assume
A4: [a,b] in R;
then a in field R & b in field R by RELAT_1:15;
then [b,a] in R by A1,A4;
hence [a,b] in R~ by RELAT_1:def 7;
end;
hence [a,b] in R iff [a,b] in R~ by A2;
end;
hence R = R~;
end;
assume R = R~;
then for a,b holds a in field R & b in field R & [a,b] in R implies [b,a]
in R by RELAT_1:def 7;
hence thesis by Def3;
end;
registration
let P,R be reflexive Relation;
cluster P \/ R -> reflexive;
coherence
proof
A1: R is_reflexive_in field R by Def9;
A2: P is_reflexive_in field P by Def9;
now
let a;
A3: now
assume a in field P;
then [a,a] in P by A2;
hence [a,a] in P \/ R by XBOOLE_0:def 3;
end;
A4: now
assume a in field R;
then [a,a] in R by A1;
hence [a,a] in P \/ R by XBOOLE_0:def 3;
end;
assume a in field(P \/ R);
then a in field P \/ field R by RELAT_1:18;
hence [a,a] in P \/ R by A3,A4,XBOOLE_0:def 3;
end;
hence P \/ R is reflexive by Def1;
end;
cluster P /\ R -> reflexive;
coherence
proof
A5: R is_reflexive_in field R by Def9;
A6: P is_reflexive_in field P by Def9;
now
let a;
assume
A7: a in field(P /\ R);
A8: field(P /\ R) c= field P /\ field R by RELAT_1:19;
then a in field R by A7,XBOOLE_0:def 4;
then
A9: [a,a] in R by A5;
a in field P by A8,A7,XBOOLE_0:def 4;
then [a,a] in P by A6;
hence [a,a] in P /\ R by A9,XBOOLE_0:def 4;
end;
hence thesis by Def1;
end;
end;
registration
let P,R be irreflexive Relation;
cluster P \/ R -> irreflexive;
coherence
proof
A1: P is_irreflexive_in field P by Def10;
A2: R is_irreflexive_in field R by Def10;
let a;
A3: now
assume a in field P;
then
A4: not [a,a] in P by A1;
A5: not a in field R implies not [a,a] in R by RELAT_1:15;
a in field R implies not [a,a] in R by A2;
hence not [a,a] in P \/ R by A4,A5,XBOOLE_0:def 3;
end;
A6: now
assume a in field R;
then
A7: not [a,a] in R by A2;
A8: not a in field P implies not [a,a] in P by RELAT_1:15;
a in field P implies not [a,a] in P by A1;
hence not [a,a] in P \/ R by A7,A8,XBOOLE_0:def 3;
end;
assume a in field(P \/ R);
then a in field P \/ field R by RELAT_1:18;
hence not [a,a] in P \/ R by A3,A6,XBOOLE_0:def 3;
end;
cluster P /\ R -> irreflexive;
coherence
proof
let a;
assume
A9: a in field(P /\ R);
field(P /\ R) c= (field P) /\ (field R) by RELAT_1:19;
then a in field P by A9,XBOOLE_0:def 4;
then not [a,a] in P by Def10,Def2;
hence thesis by XBOOLE_0:def 4;
end;
end;
registration
let P be irreflexive Relation;
let R be Relation;
cluster P \ R -> irreflexive;
coherence
proof
A1: P is_irreflexive_in field P by Def10;
let a;
A2: now
assume a in dom(P \ R);
then consider b being object such that
A3: [a,b] in P \ R by XTUPLE_0:def 12;
[a,b] in P by A3,XBOOLE_0:def 5;
then a in field P by RELAT_1:15;
hence not [a,a] in P by A1;
end;
now
assume a in rng(P \ R);
then consider b being object such that
A4: [b,a] in P \ R by XTUPLE_0:def 13;
[b,a] in P by A4,XBOOLE_0:def 5;
then a in field P by RELAT_1:15;
hence not [a,a] in P by A1;
end;
hence thesis by A2,XBOOLE_0:def 3,def 5;
end;
end;
registration
let R be symmetric Relation;
cluster R~ -> symmetric;
coherence by Th6;
end;
registration
let P,R be symmetric Relation;
cluster P \/ R -> symmetric;
coherence
proof
A1: R is_symmetric_in field R by Def11;
A2: P is_symmetric_in field P by Def11;
now
let a,b;
assume that
a in field(P \/ R) and
b in field(P \/ R) and
A3: [a,b] in P \/ R;
A4: now
assume
A5: [a,b] in R;
then a in field R & b in field R by RELAT_1:15;
then [b,a] in R by A1,A5;
hence [b,a] in P \/ R by XBOOLE_0:def 3;
end;
now
assume
A6: [a,b] in P;
then a in field P & b in field P by RELAT_1:15;
then [b,a] in P by A2,A6;
hence [b,a] in P \/ R by XBOOLE_0:def 3;
end;
hence [b,a] in P \/ R by A3,A4,XBOOLE_0:def 3;
end;
hence thesis by Def3;
end;
cluster P /\ R -> symmetric;
coherence
proof
A7: R is_symmetric_in field R by Def11;
A8: P is_symmetric_in field P by Def11;
now
let a,b;
assume that
A9: a in field(P /\ R) & b in field(P /\ R) and
A10: [a,b] in P /\ R;
A11: [a,b] in R by A10,XBOOLE_0:def 4;
A12: field(P /\ R) c= field P /\ field R by RELAT_1:19;
then a in field R & b in field R by A9,XBOOLE_0:def 4;
then
A13: [b,a] in R by A7,A11;
A14: [a,b] in P by A10,XBOOLE_0:def 4;
a in field P & b in field P by A12,A9,XBOOLE_0:def 4;
then [b,a] in P by A8,A14;
hence [b,a] in P /\ R by A13,XBOOLE_0:def 4;
end;
hence thesis by Def3;
end;
cluster P \ R -> symmetric;
coherence
proof
A15: R is_symmetric_in field R by Def11;
A16: P is_symmetric_in field P by Def11;
now
let a,b;
assume that
a in field(P \ R) and
b in field(P \ R) and
A17: [a,b] in P \ R;
not [a,b] in R by A17,XBOOLE_0:def 5;
then
A18: not b in field R or not a in field R or not [b,a] in R by A15;
A19: [a,b] in P by A17,XBOOLE_0:def 5;
then a in field P & b in field P by RELAT_1:15;
then
A20: [b,a] in P by A16,A19;
( not b in field R or not a in field R ) implies not [b,a] in R
by RELAT_1:15;
hence [b,a] in P \ R by A20,A18,XBOOLE_0:def 5;
end;
hence thesis by Def3;
end;
end;
registration
let R be asymmetric Relation;
cluster R~ -> asymmetric;
coherence
proof
A1: R is_asymmetric_in field R by Def13;
let x,y;
assume that
A2: x in field(R~) & y in field(R~) and
A3: [x,y] in R~;
A4: [y,x] in R by A3,RELAT_1:def 7;
x in field R & y in field R by A2,RELAT_1:21;
then not [x,y] in R by A1,A4;
hence thesis by RELAT_1:def 7;
end;
end;
registration
let P be Relation;
let R be asymmetric Relation;
cluster P /\ R -> asymmetric;
coherence
proof
A1: R is_asymmetric_in field R by Def13;
A2: field(P /\ R) c= (field P) /\ (field R) by RELAT_1:19;
let a,b;
assume that
A3: a in field(P /\ R) & b in field(P /\ R) and
A4: [a,b] in P /\ R;
A5: [a,b] in R by A4,XBOOLE_0:def 4;
a in field R & b in field R by A2,A3,XBOOLE_0:def 4;
then not [b,a] in R by A1,A5;
hence thesis by XBOOLE_0:def 4;
end;
cluster R /\ P -> asymmetric;
coherence;
end;
registration
let P be asymmetric Relation;
let R be Relation;
cluster P \ R -> asymmetric;
coherence
proof
A1: P is_asymmetric_in field P by Def13;
let a,b;
assume that
a in field(P \ R) and
b in field(P \ R) and
A2: [a,b] in P \ R;
A3: [a,b] in P by A2,XBOOLE_0:def 5;
then a in field P & b in field P by RELAT_1:15;
then not [b,a] in P by A1,A3;
hence thesis by XBOOLE_0:def 5;
end;
end;
::$CT 8
theorem
R is antisymmetric iff R /\ (R~) c= id (dom R)
proof
A1: now
assume R is antisymmetric;
then
A2: R is_antisymmetric_in field R;
now
let a,b be object;
assume
A3: [a,b] in R /\ (R~);
then [a,b] in R~ by XBOOLE_0:def 4;
then
A4: [b,a] in R by RELAT_1:def 7;
then
A5: b in dom R by XTUPLE_0:def 12;
A6: [a,b] in R by A3,XBOOLE_0:def 4;
then a in field R & b in field R by RELAT_1:15;
then a = b by A2,A6,A4;
hence [a,b] in id (dom R) by A5,RELAT_1:def 10;
end;
hence R /\ (R~) c= id (dom R);
end;
now
assume
A7: R /\ (R~) c= id (dom R);
now
let a,b;
assume that
a in field R and
b in field R and
A8: [a,b] in R and
A9: [b,a] in R;
[a,b] in R~ by A9,RELAT_1:def 7;
then [a,b] in R /\ (R~) by A8,XBOOLE_0:def 4;
hence a = b by A7,RELAT_1:def 10;
end;
hence R is antisymmetric by Def4;
end;
hence thesis by A1;
end;
registration
let R be antisymmetric Relation;
cluster R~ -> antisymmetric;
coherence
proof
let x,y;
assume that
A1: x in field(R~) & y in field(R~) and
A2: [x,y] in R~ & [y,x] in R~;
A3: [y,x] in R & [x,y] in R by A2,RELAT_1:def 7;
x in field R & y in field R by A1,RELAT_1:21;
hence x = y by A3,Def4,Def12;
end;
end;
registration
let P be antisymmetric Relation;
let R be Relation;
cluster P /\ R -> antisymmetric;
coherence
proof
A1: P is_antisymmetric_in field P by Def12;
let a,b;
assume that
a in field(P /\ R) & b in field(P /\ R) and
A2: [a,b] in (P /\ R) and
A3: [b,a] in (P /\ R);
A4: [b,a] in P by A3,XBOOLE_0:def 4;
A5: [a,b] in P by A2,XBOOLE_0:def 4;
then a in field P & b in field P by RELAT_1:15;
hence a = b by A1,A5,A4;
end;
cluster R /\ P -> antisymmetric;
coherence;
cluster P \ R -> antisymmetric;
coherence
proof
A6: P is_antisymmetric_in field P by Def12;
let a,b;
assume that
a in field(P \ R) & b in field(P \ R) and
A7: [a,b] in P \ R and
A8: [b,a] in P \ R;
A9: [b,a] in P by A8,XBOOLE_0:def 5;
A10: [a,b] in P by A7,XBOOLE_0:def 5;
then a in field P & b in field P by RELAT_1:15;
hence thesis by A6,A10,A9;
end;
end;
registration
let R be transitive Relation;
cluster R~ -> transitive;
coherence
proof
A1: R is_transitive_in field R by Def16;
let x,y,z;
assume that
A2: x in field(R~) & y in field(R~) and
A3: z in field(R~) and
A4: [x,y] in R~ and
A5: [y,z] in R~;
A6: x in field R & y in field R by A2,RELAT_1:21;
A7: [y,x] in R by A4,RELAT_1:def 7;
z in field R & [z,y] in R by A3,A5,RELAT_1:21,def 7;
then [z,x] in R by A1,A6,A7;
hence thesis by RELAT_1:def 7;
end;
end;
registration
let P,R be transitive Relation;
cluster P /\ R -> transitive;
coherence
proof
A1: R is_transitive_in field R by Def16;
A2: P is_transitive_in field P by Def16;
let a,b,c;
assume that
a in field(P /\ R) & b in field(P /\ R) & c in field(P /\ R) and
A3: [a,b] in P /\ R and
A4: [b,c] in P /\ R;
A5: [b,c] in R by A4,XBOOLE_0:def 4;
then
A6: c in field R by RELAT_1:15;
A7: [a,b] in R by A3,XBOOLE_0:def 4;
then a in field R & b in field R by RELAT_1:15;
then
A8: [a,c] in R by A1,A7,A5,A6;
A9: [b,c] in P by A4,XBOOLE_0:def 4;
then
A10: c in field P by RELAT_1:15;
A11: [a,b] in P by A3,XBOOLE_0:def 4;
then a in field P & b in field P by RELAT_1:15;
then [a,c] in P by A2,A11,A9,A10;
hence thesis by A8,XBOOLE_0:def 4;
end;
end;
::$CT 4
theorem
R is transitive iff R*R c= R
proof
hereby
assume R is transitive;
then
A1: R is_transitive_in field R;
now
let a,b be object;
assume [a,b] in R*R;
then consider c being object such that
A2: [a,c] in R and
A3: [c,b] in R by RELAT_1:def 8;
A4: c in field R by A2,RELAT_1:15;
a in field R & b in field R by A2,A3,RELAT_1:15;
hence [a,b] in R by A1,A2,A3,A4;
end;
hence R*R c= R;
end;
assume
A5: R*R c= R;
let a,b,c;
assume a in field R & b in field R & c in field R;
assume [a,b] in R & [b,c] in R;
then [a,c] in R*R by RELAT_1:def 8;
hence thesis by A5;
end;
theorem
R is connected iff [:field R,field R:] \ id (field R) c= R \/ R~
proof
hereby
assume R is connected;
then
A1: R is_connected_in field R;
now
let x be object;
now
assume
A2: x in [:field R, field R:] \ id (field R);
then x in [:field R, field R:] by XBOOLE_0:def 5;
then consider y,z being object such that
A3: y in field R and
A4: z in field R and
A5: x = [y,z] by ZFMISC_1:def 2;
not x in id (field R) by A2,XBOOLE_0:def 5;
then y <> z by A3,A5,RELAT_1:def 10;
then [y,z] in R or [z,y] in R by A1,A3,A4;
then [y,z] in R or [y,z] in R~ by RELAT_1:def 7;
hence x in R \/ R~ by A5,XBOOLE_0:def 3;
end;
hence x in [:field R, field R:] \ id (field R) implies x in R \/ R~;
end;
hence [:field R, field R:] \ id (field R) c= R \/ R~;
end;
assume
A6: [:field R, field R:] \ id (field R) c= R \/ R~;
let a,b;
[a,b] in [:field R, field R:] \ id (field R) implies [a,b] in R \/ R~ by A6;
then
[a,b] in [:field R, field R:] & not [a,b] in id (field R) implies
[a,b] in R \/ R~ by XBOOLE_0:def 5;
then a in field R & b in field R & a <> b implies
[a,b] in R or [a,b] in R~ by RELAT_1:def 10,XBOOLE_0:def 3,ZFMISC_1:87;
hence thesis by RELAT_1:def 7;
end;
registration
cluster strongly_connected -> connected reflexive for Relation;
coherence
proof
let R be Relation;
assume
A1: R is_strongly_connected_in field R;
then
for x,y holds x in field R & y in field R & x <> y implies ( [x,y] in R
or [y,x] in R);
hence R is connected by Def6;
let x;
thus thesis by A1;
end;
end;
::$CT
theorem
R is strongly_connected iff [:field R, field R:] = R \/ R~
proof
hereby
assume
A1: R is strongly_connected;
now
let x be object;
A2: now
assume
A3: x in R \/ R~;
then consider y,z being object such that
A4: x = [y,z] by RELAT_1:def 1;
[y,z] in R or [y,z] in R~ by A3,A4,XBOOLE_0:def 3;
then [y,z] in R or [z,y] in R by RELAT_1:def 7;
then y in field R & z in field R by RELAT_1:15;
hence x in [:field R, field R:] by A4,ZFMISC_1:87;
end;
now
assume x in [:field R, field R:];
then consider y,z being object such that
A5: y in field R & z in field R and
A6: x = [y,z] by ZFMISC_1:def 2;
[y,z] in R or [z,y] in R by A1,A5,Def7;
then [y,z] in R or [y,z] in R~ by RELAT_1:def 7;
hence x in R \/ R~ by A6,XBOOLE_0:def 3;
end;
hence x in [:field R, field R:] iff x in R \/ R~ by A2;
end;
hence [:field R, field R:] = R \/ R~;
end;
assume
A7: [:field R, field R:] = R \/ R~;
let a,b;
a in field R & b in field R implies [a,b] in R \/ R~ by A7,ZFMISC_1:87;
then a in field R & b in field R implies [a,b] in R or [a,b] in R~
by XBOOLE_0:def 3;
hence thesis by RELAT_1:def 7;
end;
theorem
R is transitive iff for x,y,z st [x,y] in R & [y,z] in R holds [x,z] in R
proof
hereby
assume
A1: R is transitive;
let x,y,z;
assume that
A2: [x,y] in R and
A3: [y,z] in R;
A4: z in field R by A3,RELAT_1:15;
x in field R & y in field R by A2,RELAT_1:15;
hence [x,z] in R by A1,A2,A3,A4,Def8;
end;
assume for x,y,z st [x,y] in R & [y,z] in R holds [x,z] in R;
then x in field R & y in field R & z in field R & [x,y] in R & [y,z] in R
implies [x,z] in R;
hence R is_transitive_in field R;
end;