relat_2.miz

    begin

    reserve X for set,

a,b,c,x,y,z for object;

    reserve P,R for Relation;

    definition

      let R, X;

      :: RELAT_2:def1

      pred R is_reflexive_in X means

      : Def1: x in X implies [x, x] in R;

      :: RELAT_2:def2

      pred R is_irreflexive_in X means

      : Def2: x in X implies not [x, x] in R;

      :: RELAT_2:def3

      pred R is_symmetric_in X means

      : Def3: x in X & y in X & [x, y] in R implies [y, x] in R;

      :: RELAT_2:def4

      pred R is_antisymmetric_in X means

      : Def4: x in X & y in X & [x, y] in R & [y, x] in R implies x = y;

      :: RELAT_2:def5

      pred R is_asymmetric_in X means x in X & y in X & [x, y] in R implies not [y, x] in R;

      :: RELAT_2:def6

      pred R is_connected_in X means

      : Def6: x in X & y in X & x <> y implies [x, y] in R or [y, x] in R;

      :: RELAT_2:def7

      pred R is_strongly_connected_in X means

      : Def7: x in X & y in X implies [x, y] in R or [y, x] in R;

      :: RELAT_2:def8

      pred R is_transitive_in X means

      : Def8: x in X & y in X & z in X & [x, y] in R & [y, z] in R implies [x, z] in R;

    end

    definition

      let R;

      :: RELAT_2:def9

      attr R is reflexive means

      : Def9: R is_reflexive_in ( field R);

      :: RELAT_2:def10

      attr R is irreflexive means

      : Def10: R is_irreflexive_in ( field R);

      :: RELAT_2:def11

      attr R is symmetric means

      : Def11: R is_symmetric_in ( field R);

      :: RELAT_2:def12

      attr R is antisymmetric means

      : Def12: R is_antisymmetric_in ( field R);

      :: RELAT_2:def13

      attr R is asymmetric means

      : Def13: R is_asymmetric_in ( field R);

      :: RELAT_2:def14

      attr R is connected means R is_connected_in ( field R);

      :: RELAT_2:def15

      attr R is strongly_connected means R is_strongly_connected_in ( field R);

      :: RELAT_2:def16

      attr R is transitive means

      : Def16: R is_transitive_in ( field R);

    end

    registration

      cluster empty -> reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive for Relation;

      coherence

      proof

        let R be Relation;

        assume

         A1: R is empty;

        thus R is reflexive

        proof

          let x;

          thus thesis by A1, RELAT_1: 40;

        end;

        thus R is irreflexive

        proof

          let x;

          thus thesis by A1;

        end;

        thus R is symmetric

        proof

          let x;

          thus thesis by A1;

        end;

        thus R is antisymmetric

        proof

          let x;

          thus thesis by A1;

        end;

        thus R is asymmetric

        proof

          let x;

          thus thesis by A1;

        end;

        thus R is connected

        proof

          let x;

          thus thesis by A1, RELAT_1: 40;

        end;

        thus R is strongly_connected

        proof

          let x;

          thus thesis by A1, RELAT_1: 40;

        end;

        let x;

        thus thesis by A1;

      end;

    end

    theorem :: RELAT_2:1

    R is reflexive iff ( id ( field R)) c= R

    proof

      hereby

        assume

         A1: R is reflexive;

        thus ( id ( field R)) c= R

        proof

          let a,b be object;

          assume [a, b] in ( id ( field R));

          then a in ( field R) & a = b by RELAT_1:def 10;

          hence [a, b] in R by A1, Def1;

        end;

      end;

      assume

       A2: ( id ( field R)) c= R;

      let a;

      assume a in ( field R);

      then [a, a] in ( id ( field R)) by RELAT_1:def 10;

      hence [a, a] in R by A2;

    end;

    theorem :: RELAT_2:2

    R is irreflexive iff ( id ( field R)) misses R

    proof

      hereby

        assume R is irreflexive;

        then

         A1: R is_irreflexive_in ( field R);

        now

          let a,b be object;

          assume

           A2: [a, b] in (( id ( field R)) /\ R);

          then [a, b] in ( id ( field R)) by XBOOLE_0:def 4;

          then

           A3: a in ( field R) & a = b by RELAT_1:def 10;

           [a, b] in R by A2, XBOOLE_0:def 4;

          hence contradiction by A1, A3;

        end;

        hence ( id ( field R)) misses R by RELAT_1: 37, XBOOLE_0:def 7;

      end;

      assume

       A4: ( id ( field R)) misses R;

      let a;

      assume a in ( field R);

      then [a, a] in ( id ( field R)) by RELAT_1:def 10;

      hence thesis by A4, XBOOLE_0: 3;

    end;

    theorem :: RELAT_2:3

    R is_antisymmetric_in X iff (R \ ( id X)) is_asymmetric_in X

    proof

      hereby

        assume

         A1: R is_antisymmetric_in X;

        thus (R \ ( id X)) is_asymmetric_in X

        proof

          let x, y;

          assume that

           A2: x in X and

           A3: y in X and

           A4: [x, y] in (R \ ( id X));

           not [x, y] in ( id X) by A4, XBOOLE_0:def 5;

          then

           A5: x <> y by A2, RELAT_1:def 10;

           [x, y] in R by A4, XBOOLE_0:def 5;

          then not [y, x] in R by A1, A2, A3, A5;

          hence not [y, x] in (R \ ( id X)) by XBOOLE_0:def 5;

        end;

      end;

      assume

       A6: (R \ ( id X)) is_asymmetric_in X;

      let x, y;

      assume that

       A7: x in X & y in X and

       A8: [x, y] in R and

       A9: [y, x] in R;

      assume

       A10: x <> y;

      then not [y, x] in ( id X) by RELAT_1:def 10;

      then

       A11: [y, x] in (R \ ( id X)) by A9, XBOOLE_0:def 5;

       not [x, y] in ( id X) by A10, RELAT_1:def 10;

      then [x, y] in (R \ ( id X)) by A8, XBOOLE_0:def 5;

      hence contradiction by A6, A7, A11;

    end;

    theorem :: RELAT_2:4

    R is_asymmetric_in X implies (R \/ ( id X)) is_antisymmetric_in X

    proof

      assume

       A1: R is_asymmetric_in X;

      let x, y;

      assume that

       A2: x in X & y in X and

       A3: [x, y] in (R \/ ( id X)) and

       A4: [y, x] in (R \/ ( id X));

      assume

       A5: x <> y;

      then not [y, x] in ( id X) by RELAT_1:def 10;

      then

       A6: [y, x] in R by A4, XBOOLE_0:def 3;

       not [x, y] in ( id X) by A5, RELAT_1:def 10;

      then [x, y] in R by A3, XBOOLE_0:def 3;

      hence contradiction by A1, A2, A6;

    end;

    ::$Canceled

    registration

      cluster symmetric transitive -> reflexive for Relation;

      coherence

      proof

        let R be Relation;

        assume that

         A1: R is symmetric and

         A2: R is transitive;



         A3: R is_transitive_in ( field R) by A2;



         A4: R is_symmetric_in ( field R) by A1;

        let a;

         A5:

        now

          assume a in ( dom R);

          then

          consider b be object such that

           A6: [a, b] in R by XTUPLE_0:def 12;



           A7: a in ( field R) & b in ( field R) by A6, RELAT_1: 15;

          then [b, a] in R by A4, A6;

          hence [a, a] in R by A3, A6, A7;

        end;

        now

          assume a in ( rng R);

          then

          consider b be object such that

           A8: [b, a] in R by XTUPLE_0:def 13;



           A9: a in ( field R) & b in ( field R) by A8, RELAT_1: 15;

          then [a, b] in R by A4, A8;

          hence [a, a] in R by A3, A8, A9;

        end;

        hence thesis by A5, XBOOLE_0:def 3;

      end;

    end

    registration

      let X;

      cluster ( id X) -> symmetric transitive antisymmetric;

      coherence

      proof

        thus ( id X) is symmetric

        proof

          let a, b;

          assume that a in ( field ( id X)) and b in ( field ( id X)) and

           A1: [a, b] in ( id X);

          a = b by A1, RELAT_1:def 10;

          hence thesis by A1;

        end;

        thus ( id X) is transitive

        proof

          let a, b, c;

          thus thesis by RELAT_1:def 10;

        end;

        thus ( id X) is antisymmetric

        proof

          let a, b;

          thus thesis by RELAT_1:def 10;

        end;

      end;

    end

    registration

      cluster irreflexive transitive -> asymmetric for Relation;

      coherence

      proof

        let R be Relation;

        assume that

         A1: R is_irreflexive_in ( field R) and

         A2: R is_transitive_in ( field R);

        let a, b;

        assume that

         A3: a in ( field R) and

         A4: b in ( field R);

         not [a, a] in R by A1, A3;

        hence thesis by A2, A3, A4;

      end;

      cluster asymmetric -> irreflexive antisymmetric for Relation;

      coherence

      proof

        let R be Relation;

        assume

         A5: R is_asymmetric_in ( field R);

        then for x holds x in ( field R) implies not [x, x] in R;

        hence R is irreflexive by Def2;

        for x, y holds x in ( field R) & y in ( field R) & [x, y] in R & [y, x] in R implies x = y by A5;

        hence thesis by Def4;

      end;

    end

    registration

      let R be reflexive Relation;

      cluster (R ~ ) -> reflexive;

      coherence

      proof



         A1: R is_reflexive_in ( field R) by Def9;

        let x;

        assume x in ( field (R ~ ));

        then x in ( field R) by RELAT_1: 21;

        then [x, x] in R by A1;

        hence [x, x] in (R ~ ) by RELAT_1:def 7;

      end;

    end

    registration

      let R be irreflexive Relation;

      cluster (R ~ ) -> irreflexive;

      coherence

      proof



         A1: R is_irreflexive_in ( field R) by Def10;

        let x;

        assume x in ( field (R ~ ));

        then x in ( field R) by RELAT_1: 21;

        then not [x, x] in R by A1;

        hence thesis by RELAT_1:def 7;

      end;

    end

    theorem :: RELAT_2:12

    R is reflexive implies ( dom R) = ( dom (R ~ )) & ( rng R) = ( rng (R ~ ))

    proof

      assume

       A1: R is reflexive;

      then

       A2: R is_reflexive_in ( field R);



       A3: (R ~ ) is_reflexive_in ( field (R ~ )) by A1, Def9;

      now

        let x be object;

         A4:

        now

          assume x in ( dom (R ~ ));

          then x in ( field (R ~ )) by XBOOLE_0:def 3;

          then [x, x] in (R ~ ) by A1, Def1, Def9;

          then [x, x] in R by RELAT_1:def 7;

          hence x in ( dom R) by XTUPLE_0:def 12;

        end;

        now

          assume x in ( dom R);

          then x in ( field R) by XBOOLE_0:def 3;

          then [x, x] in R by A1, Def1;

          then [x, x] in (R ~ ) by RELAT_1:def 7;

          hence x in ( dom (R ~ )) by XTUPLE_0:def 12;

        end;

        hence x in ( dom R) iff x in ( dom (R ~ )) by A4;

      end;

      hence ( dom R) = ( dom (R ~ )) by TARSKI: 2;

      now

        let x be object;

         A5:

        now

          assume x in ( rng (R ~ ));

          then x in ( field (R ~ )) by XBOOLE_0:def 3;

          then [x, x] in (R ~ ) by A3;

          then [x, x] in R by RELAT_1:def 7;

          hence x in ( rng R) by XTUPLE_0:def 13;

        end;

        now

          assume x in ( rng R);

          then x in ( field R) by XBOOLE_0:def 3;

          then [x, x] in R by A2;

          then [x, x] in (R ~ ) by RELAT_1:def 7;

          hence x in ( rng (R ~ )) by XTUPLE_0:def 13;

        end;

        hence x in ( rng R) iff x in ( rng (R ~ )) by A5;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: RELAT_2:13



     Th6: R is symmetric iff R = (R ~ )

    proof

      hereby

        assume R is symmetric;

        then

         A1: R is_symmetric_in ( field R);

        now

          let a,b be object;

           A2:

          now

            assume [a, b] in (R ~ );

            then

             A3: [b, a] in R by RELAT_1:def 7;

            then a in ( field R) & b in ( field R) by RELAT_1: 15;

            hence [a, b] in R by A1, A3;

          end;

          now

            assume

             A4: [a, b] in R;

            then a in ( field R) & b in ( field R) by RELAT_1: 15;

            then [b, a] in R by A1, A4;

            hence [a, b] in (R ~ ) by RELAT_1:def 7;

          end;

          hence [a, b] in R iff [a, b] in (R ~ ) by A2;

        end;

        hence R = (R ~ );

      end;

      assume R = (R ~ );

      then for a, b holds a in ( field R) & b in ( field R) & [a, b] in R implies [b, a] in R by RELAT_1:def 7;

      hence thesis by Def3;

    end;

    registration

      let P,R be reflexive Relation;

      cluster (P \/ R) -> reflexive;

      coherence

      proof



         A1: R is_reflexive_in ( field R) by Def9;



         A2: P is_reflexive_in ( field P) by Def9;

        now

          let a;

           A3:

          now

            assume a in ( field P);

            then [a, a] in P by A2;

            hence [a, a] in (P \/ R) by XBOOLE_0:def 3;

          end;

           A4:

          now

            assume a in ( field R);

            then [a, a] in R by A1;

            hence [a, a] in (P \/ R) by XBOOLE_0:def 3;

          end;

          assume a in ( field (P \/ R));

          then a in (( field P) \/ ( field R)) by RELAT_1: 18;

          hence [a, a] in (P \/ R) by A3, A4, XBOOLE_0:def 3;

        end;

        hence (P \/ R) is reflexive by Def1;

      end;

      cluster (P /\ R) -> reflexive;

      coherence

      proof



         A5: R is_reflexive_in ( field R) by Def9;



         A6: P is_reflexive_in ( field P) by Def9;

        now

          let a;

          assume

           A7: a in ( field (P /\ R));



           A8: ( field (P /\ R)) c= (( field P) /\ ( field R)) by RELAT_1: 19;

          then a in ( field R) by A7, XBOOLE_0:def 4;

          then

           A9: [a, a] in R by A5;

          a in ( field P) by A8, A7, XBOOLE_0:def 4;

          then [a, a] in P by A6;

          hence [a, a] in (P /\ R) by A9, XBOOLE_0:def 4;

        end;

        hence thesis by Def1;

      end;

    end

    registration

      let P,R be irreflexive Relation;

      cluster (P \/ R) -> irreflexive;

      coherence

      proof



         A1: P is_irreflexive_in ( field P) by Def10;



         A2: R is_irreflexive_in ( field R) by Def10;

        let a;

         A3:

        now

          assume a in ( field P);

          then

           A4: not [a, a] in P by A1;



           A5: not a in ( field R) implies not [a, a] in R by RELAT_1: 15;

          a in ( field R) implies not [a, a] in R by A2;

          hence not [a, a] in (P \/ R) by A4, A5, XBOOLE_0:def 3;

        end;

         A6:

        now

          assume a in ( field R);

          then

           A7: not [a, a] in R by A2;



           A8: not a in ( field P) implies not [a, a] in P by RELAT_1: 15;

          a in ( field P) implies not [a, a] in P by A1;

          hence not [a, a] in (P \/ R) by A7, A8, XBOOLE_0:def 3;

        end;

        assume a in ( field (P \/ R));

        then a in (( field P) \/ ( field R)) by RELAT_1: 18;

        hence not [a, a] in (P \/ R) by A3, A6, XBOOLE_0:def 3;

      end;

      cluster (P /\ R) -> irreflexive;

      coherence

      proof

        let a;

        assume

         A9: a in ( field (P /\ R));

        ( field (P /\ R)) c= (( field P) /\ ( field R)) by RELAT_1: 19;

        then a in ( field P) by A9, XBOOLE_0:def 4;

        then not [a, a] in P by Def10, Def2;

        hence thesis by XBOOLE_0:def 4;

      end;

    end

    registration

      let P be irreflexive Relation;

      let R be Relation;

      cluster (P \ R) -> irreflexive;

      coherence

      proof



         A1: P is_irreflexive_in ( field P) by Def10;

        let a;

         A2:

        now

          assume a in ( dom (P \ R));

          then

          consider b be object such that

           A3: [a, b] in (P \ R) by XTUPLE_0:def 12;

           [a, b] in P by A3, XBOOLE_0:def 5;

          then a in ( field P) by RELAT_1: 15;

          hence not [a, a] in P by A1;

        end;

        now

          assume a in ( rng (P \ R));

          then

          consider b be object such that

           A4: [b, a] in (P \ R) by XTUPLE_0:def 13;

           [b, a] in P by A4, XBOOLE_0:def 5;

          then a in ( field P) by RELAT_1: 15;

          hence not [a, a] in P by A1;

        end;

        hence thesis by A2, XBOOLE_0:def 3, XBOOLE_0:def 5;

      end;

    end

    registration

      let R be symmetric Relation;

      cluster (R ~ ) -> symmetric;

      coherence by Th6;

    end

    registration

      let P,R be symmetric Relation;

      cluster (P \/ R) -> symmetric;

      coherence

      proof



         A1: R is_symmetric_in ( field R) by Def11;



         A2: P is_symmetric_in ( field P) by Def11;

        now

          let a, b;

          assume that a in ( field (P \/ R)) and b in ( field (P \/ R)) and

           A3: [a, b] in (P \/ R);

           A4:

          now

            assume

             A5: [a, b] in R;

            then a in ( field R) & b in ( field R) by RELAT_1: 15;

            then [b, a] in R by A1, A5;

            hence [b, a] in (P \/ R) by XBOOLE_0:def 3;

          end;

          now

            assume

             A6: [a, b] in P;

            then a in ( field P) & b in ( field P) by RELAT_1: 15;

            then [b, a] in P by A2, A6;

            hence [b, a] in (P \/ R) by XBOOLE_0:def 3;

          end;

          hence [b, a] in (P \/ R) by A3, A4, XBOOLE_0:def 3;

        end;

        hence thesis by Def3;

      end;

      cluster (P /\ R) -> symmetric;

      coherence

      proof



         A7: R is_symmetric_in ( field R) by Def11;



         A8: P is_symmetric_in ( field P) by Def11;

        now

          let a, b;

          assume that

           A9: a in ( field (P /\ R)) & b in ( field (P /\ R)) and

           A10: [a, b] in (P /\ R);



           A11: [a, b] in R by A10, XBOOLE_0:def 4;



           A12: ( field (P /\ R)) c= (( field P) /\ ( field R)) by RELAT_1: 19;

          then a in ( field R) & b in ( field R) by A9, XBOOLE_0:def 4;

          then

           A13: [b, a] in R by A7, A11;



           A14: [a, b] in P by A10, XBOOLE_0:def 4;

          a in ( field P) & b in ( field P) by A12, A9, XBOOLE_0:def 4;

          then [b, a] in P by A8, A14;

          hence [b, a] in (P /\ R) by A13, XBOOLE_0:def 4;

        end;

        hence thesis by Def3;

      end;

      cluster (P \ R) -> symmetric;

      coherence

      proof



         A15: R is_symmetric_in ( field R) by Def11;



         A16: P is_symmetric_in ( field P) by Def11;

        now

          let a, b;

          assume that a in ( field (P \ R)) and b in ( field (P \ R)) and

           A17: [a, b] in (P \ R);

           not [a, b] in R by A17, XBOOLE_0:def 5;

          then

           A18: not b in ( field R) or not a in ( field R) or not [b, a] in R by A15;



           A19: [a, b] in P by A17, XBOOLE_0:def 5;

          then a in ( field P) & b in ( field P) by RELAT_1: 15;

          then

           A20: [b, a] in P by A16, A19;

          ( not b in ( field R) or not a in ( field R)) implies not [b, a] in R by RELAT_1: 15;

          hence [b, a] in (P \ R) by A20, A18, XBOOLE_0:def 5;

        end;

        hence thesis by Def3;

      end;

    end

    registration

      let R be asymmetric Relation;

      cluster (R ~ ) -> asymmetric;

      coherence

      proof



         A1: R is_asymmetric_in ( field R) by Def13;

        let x, y;

        assume that

         A2: x in ( field (R ~ )) & y in ( field (R ~ )) and

         A3: [x, y] in (R ~ );



         A4: [y, x] in R by A3, RELAT_1:def 7;

        x in ( field R) & y in ( field R) by A2, RELAT_1: 21;

        then not [x, y] in R by A1, A4;

        hence thesis by RELAT_1:def 7;

      end;

    end

    registration

      let P be Relation;

      let R be asymmetric Relation;

      cluster (P /\ R) -> asymmetric;

      coherence

      proof



         A1: R is_asymmetric_in ( field R) by Def13;



         A2: ( field (P /\ R)) c= (( field P) /\ ( field R)) by RELAT_1: 19;

        let a, b;

        assume that

         A3: a in ( field (P /\ R)) & b in ( field (P /\ R)) and

         A4: [a, b] in (P /\ R);



         A5: [a, b] in R by A4, XBOOLE_0:def 4;

        a in ( field R) & b in ( field R) by A2, A3, XBOOLE_0:def 4;

        then not [b, a] in R by A1, A5;

        hence thesis by XBOOLE_0:def 4;

      end;

      cluster (R /\ P) -> asymmetric;

      coherence ;

    end

    registration

      let P be asymmetric Relation;

      let R be Relation;

      cluster (P \ R) -> asymmetric;

      coherence

      proof



         A1: P is_asymmetric_in ( field P) by Def13;

        let a, b;

        assume that a in ( field (P \ R)) and b in ( field (P \ R)) and

         A2: [a, b] in (P \ R);



         A3: [a, b] in P by A2, XBOOLE_0:def 5;

        then a in ( field P) & b in ( field P) by RELAT_1: 15;

        then not [b, a] in P by A1, A3;

        hence thesis by XBOOLE_0:def 5;

      end;

    end

    ::$Canceled

    theorem :: RELAT_2:22

    R is antisymmetric iff (R /\ (R ~ )) c= ( id ( dom R))

    proof

       A1:

      now

        assume R is antisymmetric;

        then

         A2: R is_antisymmetric_in ( field R);

        now

          let a,b be object;

          assume

           A3: [a, b] in (R /\ (R ~ ));

          then [a, b] in (R ~ ) by XBOOLE_0:def 4;

          then

           A4: [b, a] in R by RELAT_1:def 7;

          then

           A5: b in ( dom R) by XTUPLE_0:def 12;



           A6: [a, b] in R by A3, XBOOLE_0:def 4;

          then a in ( field R) & b in ( field R) by RELAT_1: 15;

          then a = b by A2, A6, A4;

          hence [a, b] in ( id ( dom R)) by A5, RELAT_1:def 10;

        end;

        hence (R /\ (R ~ )) c= ( id ( dom R));

      end;

      now

        assume

         A7: (R /\ (R ~ )) c= ( id ( dom R));

        now

          let a, b;

          assume that a in ( field R) and b in ( field R) and

           A8: [a, b] in R and

           A9: [b, a] in R;

           [a, b] in (R ~ ) by A9, RELAT_1:def 7;

          then [a, b] in (R /\ (R ~ )) by A8, XBOOLE_0:def 4;

          hence a = b by A7, RELAT_1:def 10;

        end;

        hence R is antisymmetric by Def4;

      end;

      hence thesis by A1;

    end;

    registration

      let R be antisymmetric Relation;

      cluster (R ~ ) -> antisymmetric;

      coherence

      proof

        let x, y;

        assume that

         A1: x in ( field (R ~ )) & y in ( field (R ~ )) and

         A2: [x, y] in (R ~ ) & [y, x] in (R ~ );



         A3: [y, x] in R & [x, y] in R by A2, RELAT_1:def 7;

        x in ( field R) & y in ( field R) by A1, RELAT_1: 21;

        hence x = y by A3, Def4, Def12;

      end;

    end

    registration

      let P be antisymmetric Relation;

      let R be Relation;

      cluster (P /\ R) -> antisymmetric;

      coherence

      proof



         A1: P is_antisymmetric_in ( field P) by Def12;

        let a, b;

        assume that a in ( field (P /\ R)) & b in ( field (P /\ R)) and

         A2: [a, b] in (P /\ R) and

         A3: [b, a] in (P /\ R);



         A4: [b, a] in P by A3, XBOOLE_0:def 4;



         A5: [a, b] in P by A2, XBOOLE_0:def 4;

        then a in ( field P) & b in ( field P) by RELAT_1: 15;

        hence a = b by A1, A5, A4;

      end;

      cluster (R /\ P) -> antisymmetric;

      coherence ;

      cluster (P \ R) -> antisymmetric;

      coherence

      proof



         A6: P is_antisymmetric_in ( field P) by Def12;

        let a, b;

        assume that a in ( field (P \ R)) & b in ( field (P \ R)) and

         A7: [a, b] in (P \ R) and

         A8: [b, a] in (P \ R);



         A9: [b, a] in P by A8, XBOOLE_0:def 5;



         A10: [a, b] in P by A7, XBOOLE_0:def 5;

        then a in ( field P) & b in ( field P) by RELAT_1: 15;

        hence thesis by A6, A10, A9;

      end;

    end

    registration

      let R be transitive Relation;

      cluster (R ~ ) -> transitive;

      coherence

      proof



         A1: R is_transitive_in ( field R) by Def16;

        let x, y, z;

        assume that

         A2: x in ( field (R ~ )) & y in ( field (R ~ )) and

         A3: z in ( field (R ~ )) and

         A4: [x, y] in (R ~ ) and

         A5: [y, z] in (R ~ );



         A6: x in ( field R) & y in ( field R) by A2, RELAT_1: 21;



         A7: [y, x] in R by A4, RELAT_1:def 7;

        z in ( field R) & [z, y] in R by A3, A5, RELAT_1: 21, RELAT_1:def 7;

        then [z, x] in R by A1, A6, A7;

        hence thesis by RELAT_1:def 7;

      end;

    end

    registration

      let P,R be transitive Relation;

      cluster (P /\ R) -> transitive;

      coherence

      proof



         A1: R is_transitive_in ( field R) by Def16;



         A2: P is_transitive_in ( field P) by Def16;

        let a, b, c;

        assume that a in ( field (P /\ R)) & b in ( field (P /\ R)) & c in ( field (P /\ R)) and

         A3: [a, b] in (P /\ R) and

         A4: [b, c] in (P /\ R);



         A5: [b, c] in R by A4, XBOOLE_0:def 4;

        then

         A6: c in ( field R) by RELAT_1: 15;



         A7: [a, b] in R by A3, XBOOLE_0:def 4;

        then a in ( field R) & b in ( field R) by RELAT_1: 15;

        then

         A8: [a, c] in R by A1, A7, A5, A6;



         A9: [b, c] in P by A4, XBOOLE_0:def 4;

        then

         A10: c in ( field P) by RELAT_1: 15;



         A11: [a, b] in P by A3, XBOOLE_0:def 4;

        then a in ( field P) & b in ( field P) by RELAT_1: 15;

        then [a, c] in P by A2, A11, A9, A10;

        hence thesis by A8, XBOOLE_0:def 4;

      end;

    end

    ::$Canceled

    theorem :: RELAT_2:27

    R is transitive iff (R * R) c= R

    proof

      hereby

        assume R is transitive;

        then

         A1: R is_transitive_in ( field R);

        now

          let a,b be object;

          assume [a, b] in (R * R);

          then

          consider c be object such that

           A2: [a, c] in R and

           A3: [c, b] in R by RELAT_1:def 8;



           A4: c in ( field R) by A2, RELAT_1: 15;

          a in ( field R) & b in ( field R) by A2, A3, RELAT_1: 15;

          hence [a, b] in R by A1, A2, A3, A4;

        end;

        hence (R * R) c= R;

      end;

      assume

       A5: (R * R) c= R;

      let a, b, c;

      assume a in ( field R) & b in ( field R) & c in ( field R);

      assume [a, b] in R & [b, c] in R;

      then [a, c] in (R * R) by RELAT_1:def 8;

      hence thesis by A5;

    end;

    theorem :: RELAT_2:28

    R is connected iff ( [:( field R), ( field R):] \ ( id ( field R))) c= (R \/ (R ~ ))

    proof

      hereby

        assume R is connected;

        then

         A1: R is_connected_in ( field R);

        now

          let x be object;

          now

            assume

             A2: x in ( [:( field R), ( field R):] \ ( id ( field R)));

            then x in [:( field R), ( field R):] by XBOOLE_0:def 5;

            then

            consider y,z be object such that

             A3: y in ( field R) and

             A4: z in ( field R) and

             A5: x = [y, z] by ZFMISC_1:def 2;

             not x in ( id ( field R)) by A2, XBOOLE_0:def 5;

            then y <> z by A3, A5, RELAT_1:def 10;

            then [y, z] in R or [z, y] in R by A1, A3, A4;

            then [y, z] in R or [y, z] in (R ~ ) by RELAT_1:def 7;

            hence x in (R \/ (R ~ )) by A5, XBOOLE_0:def 3;

          end;

          hence x in ( [:( field R), ( field R):] \ ( id ( field R))) implies x in (R \/ (R ~ ));

        end;

        hence ( [:( field R), ( field R):] \ ( id ( field R))) c= (R \/ (R ~ ));

      end;

      assume

       A6: ( [:( field R), ( field R):] \ ( id ( field R))) c= (R \/ (R ~ ));

      let a, b;

       [a, b] in ( [:( field R), ( field R):] \ ( id ( field R))) implies [a, b] in (R \/ (R ~ )) by A6;

      then [a, b] in [:( field R), ( field R):] & not [a, b] in ( id ( field R)) implies [a, b] in (R \/ (R ~ )) by XBOOLE_0:def 5;

      then a in ( field R) & b in ( field R) & a <> b implies [a, b] in R or [a, b] in (R ~ ) by RELAT_1:def 10, XBOOLE_0:def 3, ZFMISC_1: 87;

      hence thesis by RELAT_1:def 7;

    end;

    registration

      cluster strongly_connected -> connected reflexive for Relation;

      coherence

      proof

        let R be Relation;

        assume

         A1: R is_strongly_connected_in ( field R);

        then for x, y holds x in ( field R) & y in ( field R) & x <> y implies ( [x, y] in R or [y, x] in R);

        hence R is connected by Def6;

        let x;

        thus thesis by A1;

      end;

    end

    ::$Canceled

    theorem :: RELAT_2:30

    R is strongly_connected iff [:( field R), ( field R):] = (R \/ (R ~ ))

    proof

      hereby

        assume

         A1: R is strongly_connected;

        now

          let x be object;

           A2:

          now

            assume

             A3: x in (R \/ (R ~ ));

            then

            consider y,z be object such that

             A4: x = [y, z] by RELAT_1:def 1;

             [y, z] in R or [y, z] in (R ~ ) by A3, A4, XBOOLE_0:def 3;

            then [y, z] in R or [z, y] in R by RELAT_1:def 7;

            then y in ( field R) & z in ( field R) by RELAT_1: 15;

            hence x in [:( field R), ( field R):] by A4, ZFMISC_1: 87;

          end;

          now

            assume x in [:( field R), ( field R):];

            then

            consider y,z be object such that

             A5: y in ( field R) & z in ( field R) and

             A6: x = [y, z] by ZFMISC_1:def 2;

             [y, z] in R or [z, y] in R by A1, A5, Def7;

            then [y, z] in R or [y, z] in (R ~ ) by RELAT_1:def 7;

            hence x in (R \/ (R ~ )) by A6, XBOOLE_0:def 3;

          end;

          hence x in [:( field R), ( field R):] iff x in (R \/ (R ~ )) by A2;

        end;

        hence [:( field R), ( field R):] = (R \/ (R ~ ));

      end;

      assume

       A7: [:( field R), ( field R):] = (R \/ (R ~ ));

      let a, b;

      a in ( field R) & b in ( field R) implies [a, b] in (R \/ (R ~ )) by A7, ZFMISC_1: 87;

      then a in ( field R) & b in ( field R) implies [a, b] in R or [a, b] in (R ~ ) by XBOOLE_0:def 3;

      hence thesis by RELAT_1:def 7;

    end;

    theorem :: RELAT_2:31

    R is transitive iff for x, y, z st [x, y] in R & [y, z] in R holds [x, z] in R

    proof

      hereby

        assume

         A1: R is transitive;

        let x, y, z;

        assume that

         A2: [x, y] in R and

         A3: [y, z] in R;



         A4: z in ( field R) by A3, RELAT_1: 15;

        x in ( field R) & y in ( field R) by A2, RELAT_1: 15;

        hence [x, z] in R by A1, A2, A3, A4, Def8;

      end;

      assume for x, y, z st [x, y] in R & [y, z] in R holds [x, z] in R;

      then x in ( field R) & y in ( field R) & z in ( field R) & [x, y] in R & [y, z] in R implies [x, z] in R;

      hence R is_transitive_in ( field R);

    end;