:: RELAT_2 semantic presentation

begin


definition
let R be Relation;
let X be set ;
predR is_reflexive_in X means :Def1: :: RELAT_2:def 1
 for x being set st x in X holds
[x,x] in R;
predR is_irreflexive_in X means :Def2: :: RELAT_2:def 2
 for x being set st x in X holds
not [x,x] in R;
predR is_symmetric_in X means :Def3: :: RELAT_2:def 3
 for x, y being set st x in X & y in X & [x,y] in R holds
[y,x] in R;
predR is_antisymmetric_in X means :Def4: :: RELAT_2:def 4
 for x, y being set st x in X & y in X & [x,y] in R & [y,x] in R holds
x = y;
predR is_asymmetric_in X means :Def5: :: RELAT_2:def 5
 for x, y being set st x in X & y in X & [x,y] in R holds
not [y,x] in R;
predR is_connected_in X means :Def6: :: RELAT_2:def 6
 for x, y being set st x in X & y in X & x <> y & not [x,y] in R holds
[y,x] in R;
predR is_strongly_connected_in X means :Def7: :: RELAT_2:def 7
 for x, y being set st x in X & y in X & not [x,y] in R holds
[y,x] in R;
predR is_transitive_in X means :Def8: :: RELAT_2:def 8
 for x, y, z being set st x in X & y in X & z in X & [x,y] in R & [y,z] in R holds
[x,z] in R;
end;

:: deftheorem Def1 defines is_reflexive_in RELAT_2:def_1_:_
 for R being Relation
for X being set holds
( R is_reflexive_in X iff for x being set st x in X holds
[x,x] in R );

:: deftheorem Def2 defines is_irreflexive_in RELAT_2:def_2_:_
 for R being Relation
for X being set holds
( R is_irreflexive_in X iff for x being set st x in X holds
not [x,x] in R );

:: deftheorem Def3 defines is_symmetric_in RELAT_2:def_3_:_
 for R being Relation
for X being set holds
( R is_symmetric_in X iff for x, y being set st x in X & y in X & [x,y] in R holds
[y,x] in R );

:: deftheorem Def4 defines is_antisymmetric_in RELAT_2:def_4_:_
 for R being Relation
for X being set holds
( R is_antisymmetric_in X iff for x, y being set st x in X & y in X & [x,y] in R & [y,x] in R holds
x = y );

:: deftheorem Def5 defines is_asymmetric_in RELAT_2:def_5_:_
 for R being Relation
for X being set holds
( R is_asymmetric_in X iff for x, y being set st x in X & y in X & [x,y] in R holds
not [y,x] in R );

:: deftheorem Def6 defines is_connected_in RELAT_2:def_6_:_
 for R being Relation
for X being set holds
( R is_connected_in X iff for x, y being set st x in X & y in X & x <> y & not [x,y] in R holds
[y,x] in R );

:: deftheorem Def7 defines is_strongly_connected_in RELAT_2:def_7_:_
 for R being Relation
for X being set holds
( R is_strongly_connected_in X iff for x, y being set st x in X & y in X & not [x,y] in R holds
[y,x] in R );

:: deftheorem Def8 defines is_transitive_in RELAT_2:def_8_:_
 for R being Relation
for X being set holds
( R is_transitive_in X iff for x, y, z being set st x in X & y in X & z in X & [x,y] in R & [y,z] in R holds
[x,z] in R );

definition
let R be Relation;
attrR is reflexive  means :Def9: :: RELAT_2:def 9
R is_reflexive_in field R;
attrR is irreflexive  means :Def10: :: RELAT_2:def 10
R is_irreflexive_in field R;
attrR is symmetric  means :Def11: :: RELAT_2:def 11
R is_symmetric_in field R;
attrR is antisymmetric  means :Def12: :: RELAT_2:def 12
R is_antisymmetric_in field R;
attrR is asymmetric  means :Def13: :: RELAT_2:def 13
R is_asymmetric_in field R;
attrR is connected  means :Def14: :: RELAT_2:def 14
R is_connected_in field R;
attrR is strongly_connected  means :Def15: :: RELAT_2:def 15
R is_strongly_connected_in field R;
attrR is transitive  means :Def16: :: RELAT_2:def 16
R is_transitive_in field R;
end;

:: deftheorem Def9 defines reflexive RELAT_2:def_9_:_
 for R being Relation holds
( R is reflexive iff R is_reflexive_in field R );

:: deftheorem Def10 defines irreflexive RELAT_2:def_10_:_
 for R being Relation holds
( R is irreflexive iff R is_irreflexive_in field R );

:: deftheorem Def11 defines symmetric RELAT_2:def_11_:_
 for R being Relation holds
( R is symmetric iff R is_symmetric_in field R );

:: deftheorem Def12 defines antisymmetric RELAT_2:def_12_:_
 for R being Relation holds
( R is antisymmetric iff R is_antisymmetric_in field R );

:: deftheorem Def13 defines asymmetric RELAT_2:def_13_:_
 for R being Relation holds
( R is asymmetric iff R is_asymmetric_in field R );

:: deftheorem Def14 defines connected RELAT_2:def_14_:_
 for R being Relation holds
( R is connected iff R is_connected_in field R );

:: deftheorem Def15 defines strongly_connected RELAT_2:def_15_:_
 for R being Relation holds
( R is strongly_connected iff R is_strongly_connected_in field R );

:: deftheorem Def16 defines transitive RELAT_2:def_16_:_
 for R being Relation holds
( R is transitive iff R is_transitive_in field R );

registration
cluster empty Relation-like  ->  reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive for set ;
coherence
 for b1 being Relation st b1 is empty holds
( b1 is reflexive & b1 is irreflexive & b1 is symmetric & b1 is antisymmetric & b1 is asymmetric & b1 is connected & b1 is strongly_connected & b1 is transitive )
proof
let R be Relation; ::_thesis: ( R is empty implies ( R is reflexive & R is irreflexive & R is symmetric & R is antisymmetric & R is asymmetric & R is connected & R is strongly_connected & R is transitive ) )
assume A1: R is empty ; ::_thesis: ( R is reflexive & R is irreflexive & R is symmetric & R is antisymmetric & R is asymmetric & R is connected & R is strongly_connected & R is transitive )
thus  R is reflexive ::_thesis: ( R is irreflexive & R is symmetric & R is antisymmetric & R is asymmetric & R is connected & R is strongly_connected & R is transitive )
proof
let x be set ; :: according to RELAT_2:def_1,RELAT_2:def_9 ::_thesis: ( x in field R implies [x,x] in R )
thus  ( x in field R implies [x,x] in R ) by A1, RELAT_1:40; ::_thesis: verum
end;
thus  R is irreflexive ::_thesis: ( R is symmetric & R is antisymmetric & R is asymmetric & R is connected & R is strongly_connected & R is transitive )
proof
let x be set ; :: according to RELAT_2:def_2,RELAT_2:def_10 ::_thesis: ( x in field R implies not [x,x] in R )
thus  ( x in field R implies not [x,x] in R ) by A1; ::_thesis: verum
end;
thus  R is symmetric ::_thesis: ( R is antisymmetric & R is asymmetric & R is connected & R is strongly_connected & R is transitive )
proof
let x be set ; :: according to RELAT_2:def_3,RELAT_2:def_11 ::_thesis: for y being set st x in field R & y in field R & [x,y] in R holds
[y,x] in R
thus  for y being set st x in field R & y in field R & [x,y] in R holds
[y,x] in R by A1; ::_thesis: verum
end;
thus  R is antisymmetric ::_thesis: ( R is asymmetric & R is connected & R is strongly_connected & R is transitive )
proof
let x be set ; :: according to RELAT_2:def_4,RELAT_2:def_12 ::_thesis: for y being set st x in field R & y in field R & [x,y] in R & [y,x] in R holds
x = y
thus  for y being set st x in field R & y in field R & [x,y] in R & [y,x] in R holds
x = y by A1; ::_thesis: verum
end;
thus  R is asymmetric ::_thesis: ( R is connected & R is strongly_connected & R is transitive )
proof
let x be set ; :: according to RELAT_2:def_5,RELAT_2:def_13 ::_thesis: for y being set st x in field R & y in field R & [x,y] in R holds
not [y,x] in R
thus  for y being set st x in field R & y in field R & [x,y] in R holds
not [y,x] in R by A1; ::_thesis: verum
end;
thus  R is connected ::_thesis: ( R is strongly_connected & R is transitive )
proof
let x be set ; :: according to RELAT_2:def_6,RELAT_2:def_14 ::_thesis: for y being set st x in field R & y in field R & x <> y & not [x,y] in R holds
[y,x] in R
thus  for y being set st x in field R & y in field R & x <> y & not [x,y] in R holds
[y,x] in R by A1, RELAT_1:40; ::_thesis: verum
end;
thus  R is strongly_connected ::_thesis: R is transitive
proof
let x be set ; :: according to RELAT_2:def_7,RELAT_2:def_15 ::_thesis: for y being set st x in field R & y in field R & not [x,y] in R holds
[y,x] in R
thus  for y being set st x in field R & y in field R & not [x,y] in R holds
[y,x] in R by A1, RELAT_1:40; ::_thesis: verum
end;
let x be set ; :: according to RELAT_2:def_8,RELAT_2:def_16 ::_thesis: for y, z being set st x in field R & y in field R & z in field R & [x,y] in R & [y,z] in R holds
[x,z] in R
thus  for y, z being set st x in field R & y in field R & z in field R & [x,y] in R & [y,z] in R holds
[x,z] in R by A1; ::_thesis: verum
end;
end;

theorem :: RELAT_2:1
for R being Relation holds
( R is reflexive iff id (field R) c= R )
proof
let R be Relation; ::_thesis: ( R is reflexive iff id (field R) c= R )
hereby  ::_thesis: ( id (field R) c= R implies R is reflexive )
assume A3: R is reflexive ; ::_thesis: id (field R) c= R
thus  id (field R) c= R ::_thesis: verum
proof
let a be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [a,b1] in id (field R) or [a,b1] in R )
let b be set ; ::_thesis: ( not [a,b] in id (field R) or [a,b] in R )
assume  [a,b] in id (field R) ; ::_thesis: [a,b] in R
then  ( a in field R & a = b ) by RELAT_1:def_10;
hence  [a,b] in R by A3, Def1, Def9; ::_thesis: verum
end;
end;
assume A2: id (field R) c= R ; ::_thesis: R is reflexive
let a be set ; :: according to RELAT_2:def_1,RELAT_2:def_9 ::_thesis: ( a in field R implies [a,a] in R )
assume  a in field R ; ::_thesis: [a,a] in R
then  [a,a] in id (field R) by RELAT_1:def_10;
hence  [a,a] in R by A2; ::_thesis: verum
end;

theorem :: RELAT_2:2
for R being Relation holds
( R is irreflexive iff id (field R) misses R )
proof
let R be Relation; ::_thesis: ( R is irreflexive iff id (field R) misses R )
hereby  ::_thesis: ( id (field R) misses R implies R is irreflexive )
assume  R is irreflexive ; ::_thesis: id (field R) misses R
then A2: R is_irreflexive_in field R by Def10;
now__::_thesis:_for_a,_b_being_set_holds_not_[a,b]_in_(id_(field_R))_/\_R
let a, b be set ; ::_thesis: not [a,b] in (id (field R)) /\ R
assume A3: [a,b] in (id (field R)) /\ R ; ::_thesis: contradiction
then  [a,b] in id (field R) by XBOOLE_0:def_4;
then A4: ( a in field R & a = b ) by RELAT_1:def_10;
 [a,b] in R by A3, XBOOLE_0:def_4;
hence  contradiction by A2, A4, Def2; ::_thesis: verum
end;
hence  id (field R) misses R by RELAT_1:37, XBOOLE_0:def_7; ::_thesis: verum
end;
assume A5: id (field R) misses R ; ::_thesis: R is irreflexive
let a be set ; :: according to RELAT_2:def_2,RELAT_2:def_10 ::_thesis: ( a in field R implies not [a,a] in R )
assume  a in field R ; ::_thesis: not [a,a] in R
then  [a,a] in id (field R) by RELAT_1:def_10;
hence  not [a,a] in R by A5, XBOOLE_0:3; ::_thesis: verum
end;

theorem :: RELAT_2:3
for X being set
for R being Relation holds
( R is_antisymmetric_in X iff R \ (id X) is_asymmetric_in X )
proof
let X be set ; ::_thesis: for R being Relation holds
( R is_antisymmetric_in X iff R \ (id X) is_asymmetric_in X )
let R be Relation; ::_thesis: ( R is_antisymmetric_in X iff R \ (id X) is_asymmetric_in X )
hereby  ::_thesis: ( R \ (id X) is_asymmetric_in X implies R is_antisymmetric_in X )
assume A1: R is_antisymmetric_in X ; ::_thesis: R \ (id X) is_asymmetric_in X
thus  R \ (id X) is_asymmetric_in X ::_thesis: verum
proof
let x be set ; :: according to RELAT_2:def_5 ::_thesis: for y being set st x in X & y in X & [x,y] in R \ (id X) holds
not [y,x] in R \ (id X)
let y be set ; ::_thesis: ( x in X & y in X & [x,y] in R \ (id X) implies not [y,x] in R \ (id X) )
assume that
A2: x in X and
A3: y in X and
A4: [x,y] in R \ (id X) ; ::_thesis: not [y,x] 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, Def4;
hence  not [y,x] in R \ (id X) by XBOOLE_0:def_5; ::_thesis: verum
end;
end;
assume A6: R \ (id X) is_asymmetric_in X ; ::_thesis: R is_antisymmetric_in X
let x be set ; :: according to RELAT_2:def_4 ::_thesis: for y being set st x in X & y in X & [x,y] in R & [y,x] in R holds
x = y
let y be set ; ::_thesis: ( x in X & y in X & [x,y] in R & [y,x] in R implies x = y )
assume that
A7: ( x in X & y in X ) and
A8: [x,y] in R and
A9: [y,x] in R ; ::_thesis: x = y
assume A10: x <> y ; ::_thesis: contradiction
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, Def5; ::_thesis: verum
end;

theorem :: RELAT_2:4
for X being set
for R being Relation st R is_asymmetric_in X holds
R \/ (id X) is_antisymmetric_in X
proof
let X be set ; ::_thesis: for R being Relation st R is_asymmetric_in X holds
R \/ (id X) is_antisymmetric_in X
let R be Relation; ::_thesis: ( R is_asymmetric_in X implies R \/ (id X) is_antisymmetric_in X )
assume A1: R is_asymmetric_in X ; ::_thesis: R \/ (id X) is_antisymmetric_in X
let x be set ; :: according to RELAT_2:def_4 ::_thesis: for y being set st x in X & y in X & [x,y] in R \/ (id X) & [y,x] in R \/ (id X) holds
x = y
let y be set ; ::_thesis: ( x in X & y in X & [x,y] in R \/ (id X) & [y,x] in R \/ (id X) implies 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) ; ::_thesis: x = y
assume A5: x <> y ; ::_thesis: contradiction
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, Def5; ::_thesis: verum
end;

theorem :: RELAT_2:5
canceled;

theorem :: RELAT_2:6
canceled;

theorem :: RELAT_2:7
canceled;

theorem :: RELAT_2:8
canceled;

theorem :: RELAT_2:9
canceled;

theorem :: RELAT_2:10
canceled;

theorem :: RELAT_2:11
canceled;

registration
cluster Relation-like symmetric transitive  ->  reflexive for set ;
coherence
 for b1 being Relation st b1 is symmetric & b1 is transitive holds
b1 is reflexive
proof
let R be Relation; ::_thesis: ( R is symmetric & R is transitive implies R is reflexive )
assume that
A1: R is symmetric and
A2: R is transitive ; ::_thesis: R is reflexive
A3: R is_transitive_in field R by A2, Def16;
A4: R is_symmetric_in field R by A1, Def11;
let a be set ; :: according to RELAT_2:def_1,RELAT_2:def_9 ::_thesis: ( a in field R implies [a,a] in R )
A5: now__::_thesis:_(_a_in_dom_R_implies_[a,a]_in_R_)
assume  a in dom R ; ::_thesis: [a,a] in R
then consider b being set  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, Def3;
hence  [a,a] in R by A3, A6, A7, Def8; ::_thesis: verum
end;
now__::_thesis:_(_a_in_rng_R_implies_[a,a]_in_R_)
assume  a in rng R ; ::_thesis: [a,a] in R
then consider b being set  such that
A9: [b,a] in R by XTUPLE_0:def_13;
A10: ( a in field R & b in field R ) by A9, RELAT_1:15;
then  [a,b] in R by A4, A9, Def3;
hence  [a,a] in R by A3, A9, A10, Def8; ::_thesis: verum
end;
hence  ( a in field R implies [a,a] in R ) by A5, XBOOLE_0:def_3; ::_thesis: verum
end;
end;

registration
let X be set ;
cluster id X ->  symmetric antisymmetric transitive ;
coherence
 ( id X is symmetric & id X is transitive & id X is antisymmetric )
proof
thus  id X is symmetric ::_thesis: ( id X is transitive & id X is antisymmetric )
proof
let a be set ; :: according to RELAT_2:def_3,RELAT_2:def_11 ::_thesis: for y being set st a in field (id X) & y in field (id X) & [a,y] in id X holds
[y,a] in id X
let b be set ; ::_thesis: ( a in field (id X) & b in field (id X) & [a,b] in id X implies [b,a] in id X )
assume that
 a in field (id X) and
 b in field (id X) and
A1: [a,b] in id X ; ::_thesis: [b,a] in id X
 a = b by A1, RELAT_1:def_10;
hence  [b,a] in id X by A1; ::_thesis: verum
end;
thus  id X is transitive ::_thesis: id X is antisymmetric
proof
let a be set ; :: according to RELAT_2:def_8,RELAT_2:def_16 ::_thesis: for y, z being set st a in field (id X) & y in field (id X) & z in field (id X) & [a,y] in id X & [y,z] in id X holds
[a,z] in id X
let b, c be set ; ::_thesis: ( a in field (id X) & b in field (id X) & c in field (id X) & [a,b] in id X & [b,c] in id X implies [a,c] in id X )
thus  ( a in field (id X) & b in field (id X) & c in field (id X) & [a,b] in id X & [b,c] in id X implies [a,c] in id X ) by RELAT_1:def_10; ::_thesis: verum
end;
thus  id X is antisymmetric ::_thesis: verum
proof
let a be set ; :: according to RELAT_2:def_4,RELAT_2:def_12 ::_thesis: for y being set st a in field (id X) & y in field (id X) & [a,y] in id X & [y,a] in id X holds
a = y
let b be set ; ::_thesis: ( a in field (id X) & b in field (id X) & [a,b] in id X & [b,a] in id X implies a = b )
thus  ( a in field (id X) & b in field (id X) & [a,b] in id X & [b,a] in id X implies a = b ) by RELAT_1:def_10; ::_thesis: verum
end;
end;
end;

registration
cluster Relation-like irreflexive transitive  ->  asymmetric for set ;
coherence
 for b1 being Relation st b1 is irreflexive & b1 is transitive holds
b1 is asymmetric
proof
let R be Relation; ::_thesis: ( R is irreflexive & R is transitive implies R is asymmetric )
assume that
A4: R is_irreflexive_in field R and
A3: R is_transitive_in field R ; :: according to RELAT_2:def_10,RELAT_2:def_16 ::_thesis: R is asymmetric
let a be set ; :: according to RELAT_2:def_5,RELAT_2:def_13 ::_thesis: for y being set st a in field R & y in field R & [a,y] in R holds
not [y,a] in R
let b be set ; ::_thesis: ( a in field R & b in field R & [a,b] in R implies not [b,a] in R )
assume that
A5: a in field R and
A6: b in field R ; ::_thesis: ( not [a,b] in R or not [b,a] in R )
 not [a,a] in R by A4, A5, Def2;
hence  ( not [a,b] in R or not [b,a] in R ) by A3, A5, A6, Def8; ::_thesis: verum
end;
cluster Relation-like asymmetric  ->  irreflexive antisymmetric for set ;
coherence
 for b1 being Relation st b1 is asymmetric holds
( b1 is irreflexive & b1 is antisymmetric )
proof
let R be Relation; ::_thesis: ( R is asymmetric implies ( R is irreflexive & R is antisymmetric ) )
assume A1: R is_asymmetric_in field R ; :: according to RELAT_2:def_13 ::_thesis: ( R is irreflexive & R is antisymmetric )
then  for x being set st x in field R holds
not [x,x] in R by Def5;
hence  R is irreflexive by Def2, Def10; ::_thesis: R is antisymmetric
 for x, y being set st x in field R & y in field R & [x,y] in R & [y,x] in R holds
x = y by A1, Def5;
hence  R is antisymmetric by Def4, Def12; ::_thesis: verum
end;
end;

registration
let R be reflexive Relation;
clusterR ~  ->  reflexive ;
coherence
 R ~ is reflexive
proof
A1: R is_reflexive_in field R by Def9;
let x be set ; :: according to RELAT_2:def_1,RELAT_2:def_9 ::_thesis: ( x in field (R ~) implies [x,x] in R ~ )
assume  x in field (R ~) ; ::_thesis: [x,x] in R ~
then  x in field R by RELAT_1:21;
then  [x,x] in R by A1, Def1;
hence  [x,x] in R ~ by RELAT_1:def_7; ::_thesis: verum
end;
end;

registration
let R be irreflexive Relation;
clusterR ~  ->  irreflexive ;
coherence
 R ~ is irreflexive
proof
A1: R is_irreflexive_in field R by Def10;
let x be set ; :: according to RELAT_2:def_2,RELAT_2:def_10 ::_thesis: ( x in field (R ~) implies not [x,x] in R ~ )
assume  x in field (R ~) ; ::_thesis: not [x,x] in R ~
then  x in field R by RELAT_1:21;
then  not [x,x] in R by A1, Def2;
hence  not [x,x] in R ~ by RELAT_1:def_7; ::_thesis: verum
end;
end;

theorem :: RELAT_2:12
for R being Relation st R is reflexive holds
( dom R = dom (R ~) & rng R = rng (R ~) )
proof
let R be Relation; ::_thesis: ( R is reflexive implies ( dom R = dom (R ~) & rng R = rng (R ~) ) )
assume A1: R is reflexive ; ::_thesis: ( dom R = dom (R ~) & rng R = rng (R ~) )
then A2: R is_reflexive_in field R by Def9;
A3: R ~ is_reflexive_in field (R ~) by A1, Def9;
now__::_thesis:_for_x_being_set_holds_
(_x_in_dom_R_iff_x_in_dom_(R_~)_)
let x be set ; ::_thesis: ( x in dom R iff x in dom (R ~) )
A4: now__::_thesis:_(_x_in_dom_(R_~)_implies_x_in_dom_R_)
assume  x in dom (R ~) ; ::_thesis: 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; ::_thesis: verum
end;
now__::_thesis:_(_x_in_dom_R_implies_x_in_dom_(R_~)_)
assume  x in dom R ; ::_thesis: 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; ::_thesis: verum
end;
hence  ( x in dom R iff x in dom (R ~) ) by A4; ::_thesis: verum
end;
hence  dom R = dom (R ~) by TARSKI:1; ::_thesis: rng R = rng (R ~)
now__::_thesis:_for_x_being_set_holds_
(_x_in_rng_R_iff_x_in_rng_(R_~)_)
let x be set ; ::_thesis: ( x in rng R iff x in rng (R ~) )
A5: now__::_thesis:_(_x_in_rng_(R_~)_implies_x_in_rng_R_)
assume  x in rng (R ~) ; ::_thesis: x in rng R
then  x in field (R ~) by XBOOLE_0:def_3;
then  [x,x] in R ~ by A3, Def1;
then  [x,x] in R by RELAT_1:def_7;
hence  x in rng R by XTUPLE_0:def_13; ::_thesis: verum
end;
now__::_thesis:_(_x_in_rng_R_implies_x_in_rng_(R_~)_)
assume  x in rng R ; ::_thesis: x in rng (R ~)
then  x in field R by XBOOLE_0:def_3;
then  [x,x] in R by A2, Def1;
then  [x,x] in R ~ by RELAT_1:def_7;
hence  x in rng (R ~) by XTUPLE_0:def_13; ::_thesis: verum
end;
hence  ( x in rng R iff x in rng (R ~) ) by A5; ::_thesis: verum
end;
hence  rng R = rng (R ~) by TARSKI:1; ::_thesis: verum
end;

theorem Th13: :: RELAT_2:13
for R being Relation holds
( R is symmetric iff R = R ~ )
proof
let R be Relation; ::_thesis: ( R is symmetric iff R = R ~ )
hereby  ::_thesis: ( R = R ~ implies R is symmetric )
assume  R is symmetric ; ::_thesis: R = R ~
then A2: R is_symmetric_in field R by Def11;
now__::_thesis:_for_a,_b_being_set_holds_
(_[a,b]_in_R_iff_[a,b]_in_R_~_)
let a, b be set ; ::_thesis: ( [a,b] in R iff [a,b] in R ~ )
A3: now__::_thesis:_(_[a,b]_in_R_~_implies_[a,b]_in_R_)
assume  [a,b] in R ~ ; ::_thesis: [a,b] in R
then A4: [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 A2, A4, Def3; ::_thesis: verum
end;
now__::_thesis:_(_[a,b]_in_R_implies_[a,b]_in_R_~_)
assume A5: [a,b] in R ; ::_thesis: [a,b] in R ~
then  ( a in field R & b in field R ) by RELAT_1:15;
then  [b,a] in R by A2, A5, Def3;
hence  [a,b] in R ~ by RELAT_1:def_7; ::_thesis: verum
end;
hence  ( [a,b] in R iff [a,b] in R ~ ) by A3; ::_thesis: verum
end;
hence  R = R ~ by RELAT_1:def_2; ::_thesis: verum
end;
assume  R = R ~ ; ::_thesis: R is symmetric
then  for a, b being set st a in field R & b in field R & [a,b] in R holds
[b,a] in R by RELAT_1:def_7;
hence  R is symmetric by Def3, Def11; ::_thesis: verum
end;

registration
let P, R be reflexive Relation;
clusterP \/ R ->  reflexive ;
coherence
 P \/ R is reflexive
proof
A3: R is_reflexive_in field R by Def9;
A4: P is_reflexive_in field P by Def9;
now__::_thesis:_for_a_being_set_st_a_in_field_(P_\/_R)_holds_
[a,a]_in_P_\/_R
let a be set ; ::_thesis: ( a in field (P \/ R) implies [a,a] in P \/ R )
A5: now__::_thesis:_(_a_in_field_P_implies_[a,a]_in_P_\/_R_)
assume  a in field P ; ::_thesis: [a,a] in P \/ R
then  [a,a] in P by A4, Def1;
hence  [a,a] in P \/ R by XBOOLE_0:def_3; ::_thesis: verum
end;
A6: now__::_thesis:_(_a_in_field_R_implies_[a,a]_in_P_\/_R_)
assume  a in field R ; ::_thesis: [a,a] in P \/ R
then  [a,a] in R by A3, Def1;
hence  [a,a] in P \/ R by XBOOLE_0:def_3; ::_thesis: verum
end;
assume  a in field (P \/ R) ; ::_thesis: [a,a] in P \/ R
then  a in (field P) \/ (field R) by RELAT_1:18;
hence  [a,a] in P \/ R by A5, A6, XBOOLE_0:def_3; ::_thesis: verum
end;
hence  P \/ R is reflexive by Def1, Def9; ::_thesis: verum
end;
clusterP /\ R ->  reflexive ;
coherence
 P /\ R is reflexive
proof
A3: R is_reflexive_in field R by Def9;
A4: P is_reflexive_in field P by Def9;
now__::_thesis:_for_a_being_set_st_a_in_field_(P_/\_R)_holds_
[a,a]_in_P_/\_R
let a be set ; ::_thesis: ( a in field (P /\ R) implies [a,a] in P /\ R )
assume A7: a in field (P /\ R) ; ::_thesis: [a,a] in 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 A3, Def1;
 a in field P by A8, A7, XBOOLE_0:def_4;
then  [a,a] in P by A4, Def1;
hence  [a,a] in P /\ R by A9, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  P /\ R is reflexive by Def1, Def9; ::_thesis: verum
end;
end;

registration
let P, R be irreflexive Relation;
clusterP \/ R ->  irreflexive ;
coherence
 P \/ R is irreflexive
proof
A3: P is_irreflexive_in field P by Def10;
A4: R is_irreflexive_in field R by Def10;
let a be set ; :: according to RELAT_2:def_2,RELAT_2:def_10 ::_thesis: ( a in field (P \/ R) implies not [a,a] in P \/ R )
A5: now__::_thesis:_(_a_in_field_P_implies_not_[a,a]_in_P_\/_R_)
assume  a in field P ; ::_thesis: not [a,a] in P \/ R
then A6: not [a,a] in P by A3, Def2;
A7: ( 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 A4, Def2;
hence  not [a,a] in P \/ R by A6, A7, XBOOLE_0:def_3; ::_thesis: verum
end;
A8: now__::_thesis:_(_a_in_field_R_implies_not_[a,a]_in_P_\/_R_)
assume  a in field R ; ::_thesis: not [a,a] in P \/ R
then A9: not [a,a] in R by A4, Def2;
A10: ( 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 A3, Def2;
hence  not [a,a] in P \/ R by A9, A10, XBOOLE_0:def_3; ::_thesis: verum
end;
assume  a in field (P \/ R) ; ::_thesis: not [a,a] in P \/ R
then  a in (field P) \/ (field R) by RELAT_1:18;
hence  not [a,a] in P \/ R by A5, A8, XBOOLE_0:def_3; ::_thesis: verum
end;
clusterP /\ R ->  irreflexive ;
coherence
 P /\ R is irreflexive
proof
let a be set ; :: according to RELAT_2:def_2,RELAT_2:def_10 ::_thesis: ( a in field (P /\ R) implies not [a,a] in P /\ R )
assume A11: a in field (P /\ R) ; ::_thesis: not [a,a] in P /\ R
 field (P /\ R) c= (field P) /\ (field R) by RELAT_1:19;
then  a in field P by A11, XBOOLE_0:def_4;
then  not [a,a] in P by Def10, Def2;
hence  not [a,a] in P /\ R by XBOOLE_0:def_4; ::_thesis: verum
end;
end;

registration
let P be irreflexive Relation;
let R be Relation;
clusterP \ R ->  irreflexive ;
coherence
 P \ R is irreflexive
proof
A1: P is_irreflexive_in field P by Def10;
let a be set ; :: according to RELAT_2:def_2,RELAT_2:def_10 ::_thesis: ( a in field (P \ R) implies not [a,a] in P \ R )
A2: now__::_thesis:_(_a_in_dom_(P_\_R)_implies_not_[a,a]_in_P_)
assume  a in dom (P \ R) ; ::_thesis: not [a,a] in P
then consider b being set  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, Def2; ::_thesis: verum
end;
now__::_thesis:_(_a_in_rng_(P_\_R)_implies_not_[a,a]_in_P_)
assume  a in rng (P \ R) ; ::_thesis: not [a,a] in P
then consider b being set  such that
A5: [b,a] in P \ R by XTUPLE_0:def_13;
 [b,a] in P by A5, XBOOLE_0:def_5;
then  a in field P by RELAT_1:15;
hence  not [a,a] in P by A1, Def2; ::_thesis: verum
end;
hence  ( a in field (P \ R) implies not [a,a] in P \ R ) by A2, XBOOLE_0:def_3, XBOOLE_0:def_5; ::_thesis: verum
end;
end;

registration
let R be symmetric Relation;
clusterR ~  ->  symmetric ;
coherence
 R ~ is symmetric by Th13;
end;

registration
let P, R be symmetric Relation;
clusterP \/ R ->  symmetric ;
coherence
 P \/ R is symmetric
proof
A3: R is_symmetric_in field R by Def11;
A4: P is_symmetric_in field P by Def11;
now__::_thesis:_for_a,_b_being_set_st_a_in_field_(P_\/_R)_&_b_in_field_(P_\/_R)_&_[a,b]_in_P_\/_R_holds_
[b,a]_in_P_\/_R
let a, b be set ; ::_thesis: ( a in field (P \/ R) & b in field (P \/ R) & [a,b] in P \/ R implies [b,a] in P \/ R )
assume that
 a in field (P \/ R) and
 b in field (P \/ R) and
A5: [a,b] in P \/ R ; ::_thesis: [b,a] in P \/ R
A6: now__::_thesis:_(_[a,b]_in_R_implies_[b,a]_in_P_\/_R_)
assume A7: [a,b] in R ; ::_thesis: [b,a] in P \/ R
then  ( a in field R & b in field R ) by RELAT_1:15;
then  [b,a] in R by A3, A7, Def3;
hence  [b,a] in P \/ R by XBOOLE_0:def_3; ::_thesis: verum
end;
now__::_thesis:_(_[a,b]_in_P_implies_[b,a]_in_P_\/_R_)
assume A8: [a,b] in P ; ::_thesis: [b,a] in P \/ R
then  ( a in field P & b in field P ) by RELAT_1:15;
then  [b,a] in P by A4, A8, Def3;
hence  [b,a] in P \/ R by XBOOLE_0:def_3; ::_thesis: verum
end;
hence  [b,a] in P \/ R by A5, A6, XBOOLE_0:def_3; ::_thesis: verum
end;
hence  P \/ R is symmetric by Def3, Def11; ::_thesis: verum
end;
clusterP /\ R ->  symmetric ;
coherence
 P /\ R is symmetric
proof
A3: R is_symmetric_in field R by Def11;
A4: P is_symmetric_in field P by Def11;
now__::_thesis:_for_a,_b_being_set_st_a_in_field_(P_/\_R)_&_b_in_field_(P_/\_R)_&_[a,b]_in_P_/\_R_holds_
[b,a]_in_P_/\_R
let a, b be set ; ::_thesis: ( a in field (P /\ R) & b in field (P /\ R) & [a,b] in P /\ R implies [b,a] in P /\ R )
assume that
A9: ( a in field (P /\ R) & b in field (P /\ R) ) and
A10: [a,b] in P /\ R ; ::_thesis: [b,a] 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 A3, A11, Def3;
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 A4, A14, Def3;
hence  [b,a] in P /\ R by A13, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  P /\ R is symmetric by Def3, Def11; ::_thesis: verum
end;
clusterP \ R ->  symmetric ;
coherence
 P \ R is symmetric
proof
A3: R is_symmetric_in field R by Def11;
A4: P is_symmetric_in field P by Def11;
now__::_thesis:_for_a,_b_being_set_st_a_in_field_(P_\_R)_&_b_in_field_(P_\_R)_&_[a,b]_in_P_\_R_holds_
[b,a]_in_P_\_R
let a, b be set ; ::_thesis: ( a in field (P \ R) & b in field (P \ R) & [a,b] in P \ R implies [b,a] in P \ R )
assume that
 a in field (P \ R) and
 b in field (P \ R) and
A15: [a,b] in P \ R ; ::_thesis: [b,a] in P \ R
 not [a,b] in R by A15, XBOOLE_0:def_5;
then A16: ( not b in field R or not a in field R or not [b,a] in R ) by A3, Def3;
A17: [a,b] in P by A15, XBOOLE_0:def_5;
then  ( a in field P & b in field P ) by RELAT_1:15;
then A18: [b,a] in P by A4, A17, Def3;
 ( ( 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 A18, A16, XBOOLE_0:def_5; ::_thesis: verum
end;
hence  P \ R is symmetric by Def3, Def11; ::_thesis: verum
end;
end;

registration
let R be asymmetric Relation;
clusterR ~  ->  asymmetric ;
coherence
 R ~ is asymmetric
proof
A1: R is_asymmetric_in field R by Def13;
let x be set ; :: according to RELAT_2:def_5,RELAT_2:def_13 ::_thesis: for y being set st x in field (R ~) & y in field (R ~) & [x,y] in R ~ holds
not [y,x] in R ~
let y be set ; ::_thesis: ( x in field (R ~) & y in field (R ~) & [x,y] in R ~ implies not [y,x] in R ~ )
assume that
A2: ( x in field (R ~) & y in field (R ~) ) and
A3: [x,y] in R ~ ; ::_thesis: not [y,x] 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, Def5;
hence  not [y,x] in R ~ by RELAT_1:def_7; ::_thesis: verum
end;
end;

registration
let P be Relation;
let R be asymmetric Relation;
clusterP /\ R ->  asymmetric ;
coherence
 P /\ R is asymmetric
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 be set ; :: according to RELAT_2:def_5,RELAT_2:def_13 ::_thesis: for y being set st a in field (P /\ R) & y in field (P /\ R) & [a,y] in P /\ R holds
not [y,a] in P /\ R
let b be set ; ::_thesis: ( a in field (P /\ R) & b in field (P /\ R) & [a,b] in P /\ R implies not [b,a] in P /\ R )
assume that
A3: ( a in field (P /\ R) & b in field (P /\ R) ) and
A4: [a,b] in P /\ R ; ::_thesis: not [b,a] 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, Def5;
hence  not [b,a] in P /\ R by XBOOLE_0:def_4; ::_thesis: verum
end;
clusterR /\ P ->  asymmetric ;
coherence
 R /\ P is asymmetric ;
end;

registration
let P be asymmetric Relation;
let R be Relation;
clusterP \ R ->  asymmetric ;
coherence
 P \ R is asymmetric
proof
A1: P is_asymmetric_in field P by Def13;
let a be set ; :: according to RELAT_2:def_5,RELAT_2:def_13 ::_thesis: for y being set st a in field (P \ R) & y in field (P \ R) & [a,y] in P \ R holds
not [y,a] in P \ R
let b be set ; ::_thesis: ( a in field (P \ R) & b in field (P \ R) & [a,b] in P \ R implies not [b,a] in P \ R )
assume that
 a in field (P \ R) and
 b in field (P \ R) and
A2: [a,b] in P \ R ; ::_thesis: not [b,a] 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, Def5;
hence  not [b,a] in P \ R by XBOOLE_0:def_5; ::_thesis: verum
end;
end;

theorem :: RELAT_2:14
canceled;

theorem :: RELAT_2:15
canceled;

theorem :: RELAT_2:16
canceled;

theorem :: RELAT_2:17
canceled;

theorem :: RELAT_2:18
canceled;

theorem :: RELAT_2:19
canceled;

theorem :: RELAT_2:20
canceled;

theorem :: RELAT_2:21
canceled;

theorem :: RELAT_2:22
for R being Relation holds
( R is antisymmetric iff R /\ (R ~) c= id (dom R) )
proof
let R be Relation; ::_thesis: ( R is antisymmetric iff R /\ (R ~) c= id (dom R) )
A1: now__::_thesis:_(_R_is_antisymmetric_implies_R_/\_(R_~)_c=_id_(dom_R)_)
assume  R is antisymmetric ; ::_thesis: R /\ (R ~) c= id (dom R)
then A2: R is_antisymmetric_in field R by Def12;
now__::_thesis:_for_a,_b_being_set_st_[a,b]_in_R_/\_(R_~)_holds_
[a,b]_in_id_(dom_R)
let a, b be set ; ::_thesis: ( [a,b] in R /\ (R ~) implies [a,b] in id (dom R) )
assume A3: [a,b] in R /\ (R ~) ; ::_thesis: [a,b] in id (dom 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, Def4;
hence  [a,b] in id (dom R) by A5, RELAT_1:def_10; ::_thesis: verum
end;
hence  R /\ (R ~) c= id (dom R) by RELAT_1:def_3; ::_thesis: verum
end;
now__::_thesis:_(_R_/\_(R_~)_c=_id_(dom_R)_implies_R_is_antisymmetric_)
assume A7: R /\ (R ~) c= id (dom R) ; ::_thesis: R is antisymmetric
now__::_thesis:_for_a,_b_being_set_st_a_in_field_R_&_b_in_field_R_&_[a,b]_in_R_&_[b,a]_in_R_holds_
a_=_b
let a, b be set ; ::_thesis: ( a in field R & b in field R & [a,b] in R & [b,a] in R implies 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 ; ::_thesis: a = b
 [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; ::_thesis: verum
end;
hence  R is antisymmetric by Def4, Def12; ::_thesis: verum
end;
hence  ( R is antisymmetric iff R /\ (R ~) c= id (dom R) ) by A1; ::_thesis: verum
end;

registration
let R be antisymmetric Relation;
clusterR ~  ->  antisymmetric ;
coherence
 R ~ is antisymmetric
proof
let x be set ; :: according to RELAT_2:def_4,RELAT_2:def_12 ::_thesis: for y being set st x in field (R ~) & y in field (R ~) & [x,y] in R ~ & [y,x] in R ~ holds
x = y
let y be set ; ::_thesis: ( x in field (R ~) & y in field (R ~) & [x,y] in R ~ & [y,x] in R ~ implies x = y )
assume that
A2: ( x in field (R ~) & y in field (R ~) ) and
A3: ( [x,y] in R ~ & [y,x] in R ~ ) ; ::_thesis: x = y
A4: ( [y,x] in R & [x,y] in R ) by A3, RELAT_1:def_7;
 ( x in field R & y in field R ) by A2, RELAT_1:21;
hence  x = y by A4, Def4, Def12; ::_thesis: verum
end;
end;

registration
let P be antisymmetric Relation;
let R be Relation;
clusterP /\ R ->  antisymmetric ;
coherence
 P /\ R is antisymmetric
proof
A1: P is_antisymmetric_in field P by Def12;
let a be set ; :: according to RELAT_2:def_4,RELAT_2:def_12 ::_thesis: for y being set st a in field (P /\ R) & y in field (P /\ R) & [a,y] in P /\ R & [y,a] in P /\ R holds
a = y
let b be set ; ::_thesis: ( a in field (P /\ R) & b in field (P /\ R) & [a,b] in P /\ R & [b,a] in P /\ R implies 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 ; ::_thesis: a = b
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, Def4; ::_thesis: verum
end;
clusterR /\ P ->  antisymmetric ;
coherence
 R /\ P is antisymmetric ;
clusterP \ R ->  antisymmetric ;
coherence
 P \ R is antisymmetric
proof
A1: P is_antisymmetric_in field P by Def12;
let a be set ; :: according to RELAT_2:def_4,RELAT_2:def_12 ::_thesis: for y being set st a in field (P \ R) & y in field (P \ R) & [a,y] in P \ R & [y,a] in P \ R holds
a = y
let b be set ; ::_thesis: ( a in field (P \ R) & b in field (P \ R) & [a,b] in P \ R & [b,a] in P \ R implies a = b )
assume that
 ( a in field (P \ R) & b in field (P \ R) ) and
A6: [a,b] in P \ R and
A7: [b,a] in P \ R ; ::_thesis: a = b
A8: [b,a] in P by A7, XBOOLE_0:def_5;
A9: [a,b] in P by A6, XBOOLE_0:def_5;
then  ( a in field P & b in field P ) by RELAT_1:15;
hence  a = b by A1, A9, A8, Def4; ::_thesis: verum
end;
end;

registration
let R be transitive Relation;
clusterR ~  ->  transitive ;
coherence
 R ~ is transitive
proof
A1: R is_transitive_in field R by Def16;
let x be set ; :: according to RELAT_2:def_8,RELAT_2:def_16 ::_thesis: for y, z being set st x in field (R ~) & y in field (R ~) & z in field (R ~) & [x,y] in R ~ & [y,z] in R ~ holds
[x,z] in R ~
let y, z be set ; ::_thesis: ( 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 ~ )
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 ~ ; ::_thesis: [x,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, RELAT_1:def_7;
then  [z,x] in R by A1, A6, A7, Def8;
hence  [x,z] in R ~ by RELAT_1:def_7; ::_thesis: verum
end;
end;

registration
let P, R be transitive Relation;
clusterP /\ R ->  transitive ;
coherence
 P /\ R is transitive
proof
A3: R is_transitive_in field R by Def16;
A4: P is_transitive_in field P by Def16;
let a be set ; :: according to RELAT_2:def_8,RELAT_2:def_16 ::_thesis: for y, z being set st a in field (P /\ R) & y in field (P /\ R) & z in field (P /\ R) & [a,y] in P /\ R & [y,z] in P /\ R holds
[a,z] in P /\ R
let b, c be set ; ::_thesis: ( a in field (P /\ R) & b in field (P /\ R) & c in field (P /\ R) & [a,b] in P /\ R & [b,c] in P /\ R implies [a,c] in P /\ R )
assume that
 ( a in field (P /\ R) & b in field (P /\ R) & c in field (P /\ R) ) and
A5: [a,b] in P /\ R and
A6: [b,c] in P /\ R ; ::_thesis: [a,c] in P /\ R
A7: [b,c] in R by A6, XBOOLE_0:def_4;
then A8: c in field R by RELAT_1:15;
A9: [a,b] in R by A5, XBOOLE_0:def_4;
then  ( a in field R & b in field R ) by RELAT_1:15;
then A10: [a,c] in R by A3, A9, A7, A8, Def8;
A11: [b,c] in P by A6, XBOOLE_0:def_4;
then A12: c in field P by RELAT_1:15;
A13: [a,b] in P by A5, XBOOLE_0:def_4;
then  ( a in field P & b in field P ) by RELAT_1:15;
then  [a,c] in P by A4, A13, A11, A12, Def8;
hence  [a,c] in P /\ R by A10, XBOOLE_0:def_4; ::_thesis: verum
end;
end;

theorem :: RELAT_2:23
canceled;

theorem :: RELAT_2:24
canceled;

theorem :: RELAT_2:25
canceled;

theorem :: RELAT_2:26
canceled;

theorem :: RELAT_2:27
for R being Relation holds
( R is transitive iff R * R c= R )
proof
let R be Relation; ::_thesis: ( R is transitive iff R * R c= R )
hereby  ::_thesis: ( R * R c= R implies R is transitive )
assume  R is transitive ; ::_thesis: R * R c= R
then A2: R is_transitive_in field R by Def16;
now__::_thesis:_for_a,_b_being_set_st_[a,b]_in_R_*_R_holds_
[a,b]_in_R
let a, b be set ; ::_thesis: ( [a,b] in R * R implies [a,b] in R )
assume  [a,b] in R * R ; ::_thesis: [a,b] in R
then consider c being set  such that
A3: [a,c] in R and
A4: [c,b] in R by RELAT_1:def_8;
A5: c in field R by A3, RELAT_1:15;
 ( a in field R & b in field R ) by A3, A4, RELAT_1:15;
hence  [a,b] in R by A2, A3, A4, A5, Def8; ::_thesis: verum
end;
hence  R * R c= R by RELAT_1:def_3; ::_thesis: verum
end;
assume A6: R * R c= R ; ::_thesis: R is transitive
let a be set ; :: according to RELAT_2:def_8,RELAT_2:def_16 ::_thesis: for y, z being set st a in field R & y in field R & z in field R & [a,y] in R & [y,z] in R holds
[a,z] in R
let b, c be set ; ::_thesis: ( a in field R & b in field R & c in field R & [a,b] in R & [b,c] in R implies [a,c] in R )
assume  ( a in field R & b in field R & c in field R ) ; ::_thesis: ( not [a,b] in R or not [b,c] in R or [a,c] in R )
assume  ( [a,b] in R & [b,c] in R ) ; ::_thesis: [a,c] in R
then  [a,c] in R * R by RELAT_1:def_8;
hence  [a,c] in R by A6; ::_thesis: verum
end;

theorem :: RELAT_2:28
for R being Relation holds
( R is connected iff [:(field R),(field R):] \ (id (field R)) c= R \/ (R ~) )
proof
let R be Relation; ::_thesis: ( R is connected iff [:(field R),(field R):] \ (id (field R)) c= R \/ (R ~) )
hereby  ::_thesis: ( [:(field R),(field R):] \ (id (field R)) c= R \/ (R ~) implies R is connected )
assume  R is connected ; ::_thesis: [:(field R),(field R):] \ (id (field R)) c= R \/ (R ~)
then A2: R is_connected_in field R by Def14;
now__::_thesis:_for_x_being_set_st_x_in_[:(field_R),(field_R):]_\_(id_(field_R))_holds_
x_in_R_\/_(R_~)
let x be set ; ::_thesis: ( x in [:(field R),(field R):] \ (id (field R)) implies x in R \/ (R ~) )
now__::_thesis:_(_x_in_[:(field_R),(field_R):]_\_(id_(field_R))_implies_x_in_R_\/_(R_~)_)
assume A3: x in [:(field R),(field R):] \ (id (field R)) ; ::_thesis: x in R \/ (R ~)
then  x in [:(field R),(field R):] by XBOOLE_0:def_5;
then consider y, z being set  such that
A4: y in field R and
A5: z in field R and
A6: x = [y,z] by ZFMISC_1:def_2;
 not x in id (field R) by A3, XBOOLE_0:def_5;
then  y <> z by A4, A6, RELAT_1:def_10;
then  ( [y,z] in R or [z,y] in R ) by A2, A4, A5, Def6;
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; ::_thesis: verum
end;
hence  ( x in [:(field R),(field R):] \ (id (field R)) implies x in R \/ (R ~) ) ; ::_thesis: verum
end;
hence  [:(field R),(field R):] \ (id (field R)) c= R \/ (R ~) by TARSKI:def_3; ::_thesis: verum
end;
assume A7: [:(field R),(field R):] \ (id (field R)) c= R \/ (R ~) ; ::_thesis: R is connected
let a be set ; :: according to RELAT_2:def_6,RELAT_2:def_14 ::_thesis: for y being set st a in field R & y in field R & a <> y & not [a,y] in R holds
[y,a] in R
let b be set ; ::_thesis: ( a in field R & b in field R & a <> b & not [a,b] in R implies [b,a] in R )
 ( [a,b] in [:(field R),(field R):] \ (id (field R)) implies [a,b] in R \/ (R ~) ) by A7;
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 & not [a,b] in R implies [a,b] in R ~ ) by RELAT_1:def_10, XBOOLE_0:def_3, ZFMISC_1:87;
hence  ( a in field R & b in field R & a <> b & not [a,b] in R implies [b,a] in R ) by RELAT_1:def_7; ::_thesis: verum
end;

registration
cluster Relation-like strongly_connected  ->  reflexive connected for set ;
coherence
 for b1 being Relation st b1 is strongly_connected holds
( b1 is connected & b1 is reflexive )
proof
let R be Relation; ::_thesis: ( R is strongly_connected implies ( R is connected & R is reflexive ) )
assume A1: R is_strongly_connected_in field R ; :: according to RELAT_2:def_15 ::_thesis: ( R is connected & R is reflexive )
then  for x, y being set st x in field R & y in field R & x <> y & not [x,y] in R holds
[y,x] in R by Def7;
hence  R is connected by Def6, Def14; ::_thesis: R is reflexive
let x be set ; :: according to RELAT_2:def_1,RELAT_2:def_9 ::_thesis: ( x in field R implies [x,x] in R )
thus  ( x in field R implies [x,x] in R ) by A1, Def7; ::_thesis: verum
end;
end;

theorem :: RELAT_2:29
canceled;

theorem :: RELAT_2:30
for R being Relation holds
( R is strongly_connected iff [:(field R),(field R):] = R \/ (R ~) )
proof
let R be Relation; ::_thesis: ( R is strongly_connected iff [:(field R),(field R):] = R \/ (R ~) )
hereby  ::_thesis: ( [:(field R),(field R):] = R \/ (R ~) implies R is strongly_connected )
assume A2: R is strongly_connected ; ::_thesis: [:(field R),(field R):] = R \/ (R ~)
now__::_thesis:_for_x_being_set_holds_
(_x_in_[:(field_R),(field_R):]_iff_x_in_R_\/_(R_~)_)
let x be set ; ::_thesis: ( x in [:(field R),(field R):] iff x in R \/ (R ~) )
A3: now__::_thesis:_(_x_in_R_\/_(R_~)_implies_x_in_[:(field_R),(field_R):]_)
assume A4: x in R \/ (R ~) ; ::_thesis: x in [:(field R),(field R):]
then consider y, z being set  such that
A5: x = [y,z] by RELAT_1:def_1;
 ( [y,z] in R or [y,z] in R ~ ) by A4, A5, 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 A5, ZFMISC_1:87; ::_thesis: verum
end;
now__::_thesis:_(_x_in_[:(field_R),(field_R):]_implies_x_in_R_\/_(R_~)_)
assume  x in [:(field R),(field R):] ; ::_thesis: x in R \/ (R ~)
then consider y, z being set  such that
A6: ( y in field R & z in field R ) and
A7: x = [y,z] by ZFMISC_1:def_2;
 ( [y,z] in R or [z,y] in R ) by A2, A6, Def7, Def15;
then  ( [y,z] in R or [y,z] in R ~ ) by RELAT_1:def_7;
hence  x in R \/ (R ~) by A7, XBOOLE_0:def_3; ::_thesis: verum
end;
hence  ( x in [:(field R),(field R):] iff x in R \/ (R ~) ) by A3; ::_thesis: verum
end;
hence  [:(field R),(field R):] = R \/ (R ~) by TARSKI:1; ::_thesis: verum
end;
assume A8: [:(field R),(field R):] = R \/ (R ~) ; ::_thesis: R is strongly_connected
let a be set ; :: according to RELAT_2:def_7,RELAT_2:def_15 ::_thesis: for y being set st a in field R & y in field R & not [a,y] in R holds
[y,a] in R
let b be set ; ::_thesis: ( a in field R & b in field R & not [a,b] in R implies [b,a] in R )
 ( a in field R & b in field R implies [a,b] in R \/ (R ~) ) by A8, ZFMISC_1:87;
then  ( a in field R & b in field R & not [a,b] in R implies [a,b] in R ~ ) by XBOOLE_0:def_3;
hence  ( a in field R & b in field R & not [a,b] in R implies [b,a] in R ) by RELAT_1:def_7; ::_thesis: verum
end;

theorem :: RELAT_2:31
for R being Relation holds
( R is transitive iff for x, y, z being set st [x,y] in R & [y,z] in R holds
[x,z] in R )
proof
let R be Relation; ::_thesis: ( R is transitive iff for x, y, z being set st [x,y] in R & [y,z] in R holds
[x,z] in R )
hereby  ::_thesis: ( ( for x, y, z being set st [x,y] in R & [y,z] in R holds
[x,z] in R ) implies R is transitive )
assume A1: R is transitive ; ::_thesis: for x, y, z being set st [x,y] in R & [y,z] in R holds
[x,z] in R
let x, y, z be set ; ::_thesis: ( [x,y] in R & [y,z] in R implies [x,z] in R )
assume that
A2: [x,y] in R and
A3: [y,z] in R ; ::_thesis: [x,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, Def16; ::_thesis: verum
end;
assume  for x, y, z being set st [x,y] in R & [y,z] in R holds
[x,z] in R ; ::_thesis: R is transitive
then  for x, y, z being set st x in field R & y in field R & z in field R & [x,y] in R & [y,z] in R holds
[x,z] in R ;
hence  R is_transitive_in field R by Def8; :: according to RELAT_2:def_16 ::_thesis: verum
end;