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