:: On the Categories Without Uniqueness of { \bf cod } and { \bf
:: dom } . Some Properties of the Morphisms and the Functors
::  by Artur Korni{\l}owicz
::
:: Received October 3, 1997
:: Copyright (c) 1997-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies ALTCAT_1, XBOOLE_0, CAT_1, RELAT_1, ALTCAT_3, CAT_3, RELAT_2,
      FUNCTOR0, FUNCT_1, FUNCT_2, ZFMISC_1, STRUCT_0, PBOOLE, MSUALG_3,
      MSUALG_6, ALTCAT_2, REALSET1, TARSKI, ALTCAT_4;
 notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, MCART_1, RELAT_1, FUNCT_1,
      FUNCT_2, BINOP_1, MULTOP_1, PBOOLE, REALSET1, STRUCT_0, MSUALG_3,
      ALTCAT_1, ALTCAT_2, ALTCAT_3, FUNCTOR0;
 constructors REALSET1, MSUALG_3, FUNCTOR0, ALTCAT_3, RELSET_1, XTUPLE_0;
 registrations SUBSET_1, RELSET_1, FUNCOP_1, STRUCT_0, FUNCT_1, RELAT_1,
      ALTCAT_1, ALTCAT_2, FUNCTOR0, FUNCTOR2, PBOOLE, XTUPLE_0;
 requirements SUBSET, BOOLE;
 definitions ALTCAT_1, ALTCAT_3, FUNCTOR0, MSUALG_3, TARSKI, FUNCT_2, XBOOLE_0,
      PBOOLE, BINOP_1, REALSET1, ALTCAT_2, XTUPLE_0;
 theorems ALTCAT_1, ALTCAT_2, ALTCAT_3, FUNCT_1, FUNCT_2, FUNCTOR0, MCART_1,
      MULTOP_1, FUNCTOR1, FUNCTOR2, MSUALG_3, PBOOLE, RELAT_1, ZFMISC_1,
      XBOOLE_0, XBOOLE_1, PARTFUN1, XTUPLE_0;
 schemes PBOOLE, XBOOLE_0;

begin  :: Preliminaries

reserve C for category,
  o1, o2, o3 for object of C;

registration
  let C be with_units non empty AltCatStr, o be object of C;
  cluster <^o,o^> -> non empty;
  coherence by ALTCAT_1:19;
end;

theorem Th1:
  for v being Morphism of o1, o2, u being Morphism of o1, o3 for f
being Morphism of o2, o3 st u = f * v & f" * f = idm o2 & <^o1,o2^> <> {} & <^
  o2,o3^> <> {} & <^o3,o2^> <> {} holds v = f" * u
proof
  let v be Morphism of o1, o2, u be Morphism of o1, o3, f be Morphism of o2,
  o3 such that
A1: u = f * v and
A2: f" * f = idm o2 and
A3: <^o1,o2^> <> {} and
A4: <^o2,o3^> <> {} & <^o3,o2^> <> {};
  thus f" * u = f" * f * v by A1,A3,A4,ALTCAT_1:21
    .= v by A2,A3,ALTCAT_1:20;
end;

theorem Th2:
  for v being Morphism of o2, o3, u being Morphism of o1, o3 for f
being Morphism of o1, o2 st u = v * f & f * f" = idm o2 & <^o1,o2^> <> {} & <^
  o2,o1^> <> {} & <^o2,o3^> <> {} holds v = u * f"
proof
  let v be Morphism of o2, o3, u be Morphism of o1, o3, f be Morphism of o1,
  o2 such that
A1: u = v * f and
A2: f * f" = idm o2 and
A3: <^o1,o2^> <> {} & <^o2,o1^> <> {} and
A4: <^o2,o3^> <> {};
  thus u * f" = v * (f * f") by A1,A3,A4,ALTCAT_1:21
    .= v by A2,A4,ALTCAT_1:def 17;
end;

theorem Th3:
  for m being Morphism of o1, o2 st <^o1,o2^> <> {} & <^o2,o1^> <>
  {} & m is iso holds m" is iso
proof
  let m be Morphism of o1, o2 such that
A1: <^o1,o2^> <> {} & <^o2,o1^> <> {};
  assume m is iso;
  then
A2: m is retraction coretraction by ALTCAT_3:5;
  hence m"*(m")" = m" * m by A1,ALTCAT_3:3
    .= idm o1 by A1,A2,ALTCAT_3:2;
  thus (m")"*m" = m * m" by A1,A2,ALTCAT_3:3
    .= idm o2 by A1,A2,ALTCAT_3:2;
end;

theorem Th4:
  for C being with_units non empty AltCatStr, o being object of C
  holds idm o is epi mono
proof
  let C be with_units non empty AltCatStr, o be object of C;
  thus idm o is epi
  proof
    let o1 be object of C such that
A1: <^o,o1^> <> {};
    let B, C be Morphism of o, o1 such that
A2: B * idm o = C * idm o;
    thus B = B * idm o by A1,ALTCAT_1:def 17
      .= C by A1,A2,ALTCAT_1:def 17;
  end;
  let o1 be object of C such that
A3: <^o1,o^> <> {};
  let B, C be Morphism of o1, o such that
A4: idm o * B = idm o * C;
  thus B = idm o * B by A3,ALTCAT_1:20
    .= C by A3,A4,ALTCAT_1:20;
end;

registration
  let C be with_units non empty AltCatStr, o be object of C;
  cluster idm o -> epi mono retraction coretraction;
  coherence by Th4,ALTCAT_3:1;
end;

registration
  let C be category, o be object of C;
  cluster idm o -> iso;
  coherence by ALTCAT_3:6;
end;

theorem
  for f being Morphism of o1, o2, g, h being Morphism of o2, o1 st h * f
  = idm o1 & f * g = idm o2 & <^o1,o2^> <> {} & <^o2,o1^> <> {} holds g = h
proof
  let f be Morphism of o1, o2, g, h be Morphism of o2, o1 such that
A1: h * f = idm o1 and
A2: f * g = idm o2 & <^o1,o2^> <> {} and
A3: <^o2,o1^> <> {};
  thus g = h * f * g by A1,A3,ALTCAT_1:20
    .= h * idm o2 by A2,A3,ALTCAT_1:21
    .= h by A3,ALTCAT_1:def 17;
end;

theorem
  (for o1, o2 being object of C, f being Morphism of o1, o2 holds f is
  coretraction) implies for a, b being object of C, g being Morphism of a, b st
  <^a,b^> <> {} & <^b,a^> <> {} holds g is iso
proof
  assume
A1: for o1, o2 being object of C, f being Morphism of o1, o2 holds f is
  coretraction;
  let a, b be object of C, g be Morphism of a, b such that
A2: <^a,b^> <> {} and
A3: <^b,a^> <> {};
A4: g is coretraction by A1;
  g is retraction
  proof
    consider f be Morphism of b, a such that
A5: f is_left_inverse_of g by A4,ALTCAT_3:def 3;
    take f;
A6: f is mono by A1,A2,A3,ALTCAT_3:16;
    f * (g * f) = f * g * f by A2,A3,ALTCAT_1:21
      .= idm a * f by A5,ALTCAT_3:def 1
      .= f by A3,ALTCAT_1:20
      .= f * idm b by A3,ALTCAT_1:def 17;
    hence g * f = idm b by A6,ALTCAT_3:def 7;
  end;
  hence thesis by A2,A3,A4,ALTCAT_3:6;
end;

begin  :: Some properties of the initial and terminal objects

theorem
  for m, m9 being Morphism of o1, o2 st m is _zero & m9 is _zero & ex O
  being object of C st O is _zero holds m = m9
proof
  let m, m9 be Morphism of o1, o2 such that
A1: m is _zero and
A2: m9 is _zero;
  given O being object of C such that
A3: O is _zero;
  set n = the Morphism of O, O;
  set b = the Morphism of O, o2;
  set a = the Morphism of o1, O;
  thus m = b * (n" * n) * a by A1,A3,ALTCAT_3:def 12
    .= m9 by A2,A3,ALTCAT_3:def 12;
end;

theorem
  for C being non empty AltCatStr, O, A being object of C for M being
  Morphism of O, A st O is terminal holds M is mono
proof
  let C be non empty AltCatStr, O, A be object of C, M be Morphism of O, A
  such that
A1: O is terminal;
  let o be object of C such that
A2: <^o,O^> <> {};
  let a, b be Morphism of o, O such that
  M * a = M * b;
  consider N being Morphism of o, O such that
  N in <^o,O^> and
A3: for M1 being Morphism of o, O st M1 in <^o,O^> holds N = M1 by A1,
ALTCAT_3:27;
  thus a = N by A2,A3
    .= b by A2,A3;
end;

theorem
  for C being non empty AltCatStr, O, A being object of C for M being
  Morphism of A, O st O is initial holds M is epi
proof
  let C be non empty AltCatStr, O, A be object of C, M be Morphism of A, O
  such that
A1: O is initial;
  let o be object of C such that
A2: <^O,o^> <> {};
  let a, b be Morphism of O, o such that
  a * M = b * M;
  consider N being Morphism of O, o such that
  N in <^O,o^> and
A3: for M1 being Morphism of O, o st M1 in <^O,o^> holds N = M1 by A1,
ALTCAT_3:25;
  thus a = N by A2,A3
    .= b by A2,A3;
end;

theorem
  o2 is terminal & o1, o2 are_iso implies o1 is terminal
proof
  assume that
A1: o2 is terminal and
A2: o1, o2 are_iso;
  for o3 being object of C holds ex M being Morphism of o3, o1 st M in <^
  o3,o1^> & for v being Morphism of o3, o1 st v in <^o3,o1^> holds M = v
  proof
    consider f being Morphism of o1, o2 such that
A3: f is iso by A2,ALTCAT_3:def 6;
A4: f" * f = idm o1 by A3,ALTCAT_3:def 5;
    let o3 be object of C;
    consider u being Morphism of o3, o2 such that
A5: u in <^o3,o2^> and
A6: for M1 being Morphism of o3, o2 st M1 in <^o3,o2^> holds u = M1 by A1,
ALTCAT_3:27;
    take f" * u;
A7: <^o2,o1^> <> {} by A2,ALTCAT_3:def 6;
    then
A8: <^o3,o1^> <> {} by A5,ALTCAT_1:def 2;
    hence f" * u in <^o3,o1^>;
A9: <^o1,o2^> <> {} by A2,ALTCAT_3:def 6;
    let v be Morphism of o3, o1 such that
    v in <^o3,o1^>;
    f * v = u by A5,A6;
    hence thesis by A4,A9,A7,A8,Th1;
  end;
  hence thesis by ALTCAT_3:27;
end;

theorem
  o1 is initial & o1, o2 are_iso implies o2 is initial
proof
  assume that
A1: o1 is initial and
A2: o1, o2 are_iso;
  for o3 being object of C holds ex M being Morphism of o2, o3 st M in <^
  o2,o3^> & for v being Morphism of o2, o3 st v in <^o2,o3^> holds M = v
  proof
    consider f being Morphism of o1, o2 such that
A3: f is iso by A2,ALTCAT_3:def 6;
A4: f * f" = idm o2 by A3,ALTCAT_3:def 5;
    let o3 be object of C;
    consider u being Morphism of o1, o3 such that
A5: u in <^o1,o3^> and
A6: for M1 being Morphism of o1, o3 st M1 in <^o1,o3^> holds u = M1 by A1,
ALTCAT_3:25;
    take u * f";
A7: <^o2,o1^> <> {} by A2,ALTCAT_3:def 6;
    then
A8: <^o2,o3^> <> {} by A5,ALTCAT_1:def 2;
    hence u * f" in <^o2,o3^>;
A9: <^o1,o2^> <> {} by A2,ALTCAT_3:def 6;
    let v be Morphism of o2, o3 such that
    v in <^o2,o3^>;
    v * f = u by A5,A6;
    hence thesis by A4,A9,A7,A8,Th2;
  end;
  hence thesis by ALTCAT_3:25;
end;

theorem
  o1 is initial & o2 is terminal & <^o2,o1^> <> {} implies o2 is initial
  & o1 is terminal
proof
  assume that
A1: o1 is initial and
A2: o2 is terminal;
  consider l being Morphism of o1, o2 such that
A3: l in <^o1,o2^> and
  for M1 being Morphism of o1, o2 st M1 in <^o1,o2^> holds l = M1 by A1,
ALTCAT_3:25;
  assume <^o2,o1^> <> {};
  then consider m being set such that
A4: m in <^o2,o1^> by XBOOLE_0:def 1;
  reconsider m as Morphism of o2, o1 by A4;
  for o3 being object of C holds ex M being Morphism of o2, o3 st M in <^
  o2,o3^> & for M1 being Morphism of o2, o3 st M1 in <^o2,o3^> holds M = M1
  proof
    let o3 be object of C;
    consider M being Morphism of o1, o3 such that
A5: M in <^o1,o3^> and
A6: for M1 being Morphism of o1, o3 st M1 in <^o1,o3^> holds M = M1 by A1,
ALTCAT_3:25;
    take M * m;
    <^o2,o3^> <> {} by A4,A5,ALTCAT_1:def 2;
    hence M * m in <^o2,o3^>;
    let M1 be Morphism of o2, o3 such that
A7: M1 in <^o2,o3^>;
    consider i2 being Morphism of o2, o2 such that
    i2 in <^o2,o2^> and
A8: for M1 being Morphism of o2, o2 st M1 in <^o2,o2^> holds i2 = M1
    by A2,ALTCAT_3:27;
    thus M * m = M1 * l * m by A5,A6
      .= M1 * (l * m) by A4,A3,A7,ALTCAT_1:21
      .= M1 * i2 by A8
      .= M1 * idm o2 by A8
      .= M1 by A7,ALTCAT_1:def 17;
  end;
  hence o2 is initial by ALTCAT_3:25;
  for o3 being object of C holds ex M being Morphism of o3, o1 st M in <^
  o3,o1^> & for M1 being Morphism of o3, o1 st M1 in <^o3,o1^> holds M = M1
  proof
    let o3 be object of C;
    consider M being Morphism of o3, o2 such that
A9: M in <^o3,o2^> and
A10: for M1 being Morphism of o3, o2 st M1 in <^o3,o2^> holds M = M1
    by A2,ALTCAT_3:27;
    take m * M;
    <^o3,o1^> <> {} by A4,A9,ALTCAT_1:def 2;
    hence m * M in <^o3,o1^>;
    let M1 be Morphism of o3, o1 such that
A11: M1 in <^o3,o1^>;
    consider i1 being Morphism of o1, o1 such that
    i1 in <^o1,o1^> and
A12: for M1 being Morphism of o1, o1 st M1 in <^o1,o1^> holds i1 = M1
    by A1,ALTCAT_3:25;
    thus m * M = m * (l * M1) by A9,A10
      .= m * l * M1 by A4,A3,A11,ALTCAT_1:21
      .= i1 * M1 by A12
      .= idm o1 * M1 by A12
      .= M1 by A11,ALTCAT_1:20;
  end;
  hence thesis by ALTCAT_3:27;
end;

begin  :: The properties of the functors

theorem Th13:
  for A, B being transitive with_units non empty AltCatStr for F
being contravariant Functor of A, B for a being object of A holds F.idm a = idm
  (F.a)
proof
  let A, B be transitive with_units non empty AltCatStr, F be contravariant
  Functor of A, B;
  let a be object of A;
  thus F.idm a = Morph-Map(F,a,a).idm a by FUNCTOR0:def 16
    .= idm (F.a) by FUNCTOR0:def 20;
end;

theorem Th14:
  for C1, C2 being non empty AltCatStr for F being Contravariant
FunctorStr over C1, C2 holds F is full iff for o1, o2 being object of C1 holds
  Morph-Map(F,o2,o1) is onto
proof
  let C1, C2 be non empty AltCatStr, F be Contravariant FunctorStr over C1, C2;
  set I = [:the carrier of C1, the carrier of C1:];
  hereby
    assume
A1: F is full;
    let o1, o2 be object of C1;
    thus Morph-Map(F,o2,o1) is onto
    proof
A2:   [o2,o1] in I by ZFMISC_1:87;
      then
A3:   [o2,o1] in dom(the ObjectMap of F) by FUNCT_2:def 1;
      consider f being ManySortedFunction of the Arrows of C1, (the Arrows of
      C2)*the ObjectMap of F such that
A4:   f = the MorphMap of F and
A5:   f is "onto" by A1,FUNCTOR0:def 32;
      rng(f.[o2,o1]) = ((the Arrows of C2)*the ObjectMap of F).[o2,o1] by A5,A2
,MSUALG_3:def 3;
      hence
      rng(Morph-Map(F,o2,o1)) = (the Arrows of C2).((the ObjectMap of F).
      (o2,o1)) by A4,A3,FUNCT_1:13
        .= <^F.o1,F.o2^> by FUNCTOR0:23;
    end;
  end;
  assume
A6: for o1,o2 being object of C1 holds Morph-Map(F,o2,o1) is onto;
  ex I29 being non empty set, B9 being ManySortedSet of I29, f9 being
  Function of I, I29 st the ObjectMap of F = f9 & the Arrows of C2 = B9 & the
MorphMap of F is ManySortedFunction of the Arrows of C1, B9*f9 by
FUNCTOR0:def 3;
  then reconsider
  f = the MorphMap of F as ManySortedFunction of the Arrows of C1,
  (the Arrows of C2)*the ObjectMap of F;
  take f;
  thus f = the MorphMap of F;
  let i be set;
  assume i in I;
  then consider o2, o1 being set such that
A7: o2 in the carrier of C1 & o1 in the carrier of C1 and
A8: i = [o2,o1] by ZFMISC_1:84;
  reconsider o1, o2 as object of C1 by A7;
  [o2,o1] in I by ZFMISC_1:87;
  then
A9: [o2,o1] in dom(the ObjectMap of F) by FUNCT_2:def 1;
  Morph-Map(F,o2,o1) is onto by A6;
  then rng(Morph-Map(F,o2,o1)) = (the Arrows of C2).(F.o1,F.o2) by
FUNCT_2:def 3
    .= (the Arrows of C2).((the ObjectMap of F).(o2,o1)) by FUNCTOR0:23
    .= ((the Arrows of C2)*the ObjectMap of F).[o2,o1] by A9,FUNCT_1:13;
  hence thesis by A8;
end;

theorem Th15:
  for C1, C2 being non empty AltCatStr for F being Contravariant
  FunctorStr over C1, C2 holds F is faithful iff for o1, o2 being object of C1
  holds Morph-Map(F,o2,o1) is one-to-one
proof
  let C1, C2 be non empty AltCatStr, F be Contravariant FunctorStr over C1,C2;
  set I = [:the carrier of C1, the carrier of C1:];
  hereby
    assume F is faithful;
    then
A1: (the MorphMap of F) is "1-1" by FUNCTOR0:def 30;
    let o1, o2 be object of C1;
    [o2,o1] in I & dom(the MorphMap of F) = I by PARTFUN1:def 2,ZFMISC_1:87;
    hence Morph-Map(F,o2,o1) is one-to-one by A1,MSUALG_3:def 2;
  end;
  assume
A2: for o1, o2 being object of C1 holds Morph-Map(F,o2,o1) is one-to-one;
  let i be set, f be Function such that
A3: i in dom(the MorphMap of F) and
A4: (the MorphMap of F).i = f;
  dom(the MorphMap of F) = I by PARTFUN1:def 2;
  then consider o1, o2 being set such that
A5: o1 in the carrier of C1 & o2 in the carrier of C1 and
A6: i = [o1,o2] by A3,ZFMISC_1:84;
  reconsider o1, o2 as object of C1 by A5;
  (the MorphMap of F).(o1,o2) = Morph-Map(F,o1,o2);
  hence thesis by A2,A4,A6;
end;

theorem Th16:
  for C1, C2 being non empty AltCatStr for F being Covariant
FunctorStr over C1, C2 for o1, o2 being object of C1, Fm being Morphism of F.o1
, F.o2 st <^o1,o2^> <> {} & F is full feasible ex m being Morphism of o1, o2 st
  Fm = F.m
proof
  let C1, C2 be non empty AltCatStr, F be Covariant FunctorStr over C1, C2, o1
  , o2 be object of C1, Fm be Morphism of F.o1, F.o2 such that
A1: <^o1,o2^> <> {};
  assume F is full;
  then Morph-Map(F,o1,o2) is onto by FUNCTOR1:15;
  then
A2: rng Morph-Map(F,o1,o2) = <^F.o1,F.o2^> by FUNCT_2:def 3;
  assume F is feasible;
  then
A3: <^F.o1,F.o2^> <> {} by A1,FUNCTOR0:def 18;
  then consider m being set such that
A4: m in dom Morph-Map(F,o1,o2) and
A5: Fm = Morph-Map(F,o1,o2).m by A2,FUNCT_1:def 3;
  reconsider m as Morphism of o1, o2 by A3,A4,FUNCT_2:def 1;
  take m;
  thus thesis by A1,A3,A5,FUNCTOR0:def 15;
end;

theorem Th17:
  for C1, C2 being non empty AltCatStr for F being Contravariant
FunctorStr over C1, C2 for o1, o2 being object of C1, Fm being Morphism of F.o2
, F.o1 st <^o1,o2^> <> {} & F is full feasible ex m being Morphism of o1, o2 st
  Fm = F.m
proof
  let C1, C2 be non empty AltCatStr, F be Contravariant FunctorStr over C1, C2
  , o1, o2 be object of C1, Fm be Morphism of F.o2, F.o1 such that
A1: <^o1,o2^> <> {};
  assume F is full;
  then Morph-Map(F,o1,o2) is onto by Th14;
  then
A2: rng Morph-Map(F,o1,o2) = <^F.o2,F.o1^> by FUNCT_2:def 3;
  assume F is feasible;
  then
A3: <^F.o2,F.o1^> <> {} by A1,FUNCTOR0:def 19;
  then consider m being set such that
A4: m in dom Morph-Map(F,o1,o2) and
A5: Fm = Morph-Map(F,o1,o2).m by A2,FUNCT_1:def 3;
  reconsider m as Morphism of o1, o2 by A3,A4,FUNCT_2:def 1;
  take m;
  thus thesis by A1,A3,A5,FUNCTOR0:def 16;
end;

theorem Th18:
  for A, B being transitive with_units non empty AltCatStr for F
being covariant Functor of A, B for o1, o2 being object of A, a being Morphism
  of o1, o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is retraction holds F.a is
  retraction
proof
  let A, B be transitive with_units non empty AltCatStr, F be covariant
  Functor of A, B, o1, o2 be object of A, a be Morphism of o1, o2 such that
A1: <^o1,o2^> <> {} & <^o2,o1^> <> {};
  assume a is retraction;
  then consider b being Morphism of o2, o1 such that
A2: b is_right_inverse_of a by ALTCAT_3:def 2;
  take F.b;
  a * b = idm o2 by A2,ALTCAT_3:def 1;
  hence (F.a) * (F.b) = F.idm o2 by A1,FUNCTOR0:def 23
    .= idm F.o2 by FUNCTOR2:1;
end;

theorem Th19:
  for A, B being transitive with_units non empty AltCatStr for F
being covariant Functor of A, B for o1, o2 being object of A, a being Morphism
of o1, o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is coretraction holds F.a is
  coretraction
proof
  let A, B be transitive with_units non empty AltCatStr, F be covariant
  Functor of A, B, o1, o2 be object of A, a be Morphism of o1, o2 such that
A1: <^o1,o2^> <> {} & <^o2,o1^> <> {};
  assume a is coretraction;
  then consider b being Morphism of o2, o1 such that
A2: a is_right_inverse_of b by ALTCAT_3:def 3;
  take F.b;
  b * a = idm o1 by A2,ALTCAT_3:def 1;
  hence (F.b) * (F.a) = F.idm o1 by A1,FUNCTOR0:def 23
    .= idm F.o1 by FUNCTOR2:1;
end;

theorem Th20:
  for A, B being category, F being covariant Functor of A, B for
o1, o2 being object of A, a being Morphism of o1, o2 st <^o1,o2^> <> {} & <^o2,
  o1^> <> {} & a is iso holds F.a is iso
proof
  let A, B be category, F be covariant Functor of A, B, o1, o2 be object of A,
  a be Morphism of o1, o2 such that
A1: <^o1,o2^> <> {} & <^o2,o1^> <> {} and
A2: a is iso;
  a is retraction coretraction by A1,A2,ALTCAT_3:6;
  then
A3: F.a is retraction coretraction by A1,Th18,Th19;
  <^F.o1,F.o2^> <> {} & <^F.o2,F.o1^> <> {} by A1,FUNCTOR0:def 18;
  hence thesis by A3,ALTCAT_3:6;
end;

theorem
  for A, B being category, F being covariant Functor of A, B for o1, o2
  being object of A st o1, o2 are_iso holds F.o1, F.o2 are_iso
proof
  let A, B be category, F be covariant Functor of A, B, o1, o2 be object of A;
  assume
A1: o1, o2 are_iso;
  then consider a being Morphism of o1, o2 such that
A2: a is iso by ALTCAT_3:def 6;
A3: <^o1,o2^> <> {} & <^o2,o1^> <> {} by A1,ALTCAT_3:def 6;
  hence <^F.o1,F.o2^> <> {} & <^F.o2,F.o1^> <> {} by FUNCTOR0:def 18;
  take F.a;
  thus thesis by A3,A2,Th20;
end;

theorem Th22:
  for A, B being transitive with_units non empty AltCatStr for F
  being contravariant Functor of A, B for o1, o2 being object of A, a being
Morphism of o1, o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is retraction holds
  F.a is coretraction
proof
  let A, B be transitive with_units non empty AltCatStr, F be contravariant
  Functor of A, B, o1, o2 be object of A, a be Morphism of o1, o2 such that
A1: <^o1,o2^> <> {} & <^o2,o1^> <> {};
  assume a is retraction;
  then consider b being Morphism of o2, o1 such that
A2: b is_right_inverse_of a by ALTCAT_3:def 2;
  take F.b;
  a * b = idm o2 by A2,ALTCAT_3:def 1;
  hence (F.b) * (F.a) = F.idm o2 by A1,FUNCTOR0:def 24
    .= idm F.o2 by Th13;
end;

theorem Th23:
  for A, B being transitive with_units non empty AltCatStr for F
  being contravariant Functor of A, B for o1, o2 being object of A, a being
  Morphism of o1, o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is coretraction
  holds F.a is retraction
proof
  let A, B be transitive with_units non empty AltCatStr, F be contravariant
  Functor of A, B, o1, o2 be object of A, a be Morphism of o1, o2 such that
A1: <^o1,o2^> <> {} & <^o2,o1^> <> {};
  assume a is coretraction;
  then consider b being Morphism of o2, o1 such that
A2: a is_right_inverse_of b by ALTCAT_3:def 3;
  take F.b;
  b * a = idm o1 by A2,ALTCAT_3:def 1;
  hence (F.a) * (F.b) = F.idm o1 by A1,FUNCTOR0:def 24
    .= idm F.o1 by Th13;
end;

theorem Th24:
  for A, B being category, F being contravariant Functor of A, B
  for o1, o2 being object of A, a being Morphism of o1, o2 st <^o1,o2^> <> {} &
  <^o2,o1^> <> {} & a is iso holds F.a is iso
proof
  let A, B be category, F be contravariant Functor of A, B, o1, o2 be object
  of A, a be Morphism of o1, o2 such that
A1: <^o1,o2^> <> {} & <^o2,o1^> <> {} and
A2: a is iso;
  a is retraction coretraction by A1,A2,ALTCAT_3:6;
  then
A3: F.a is retraction coretraction by A1,Th22,Th23;
  <^F.o1,F.o2^> <> {} & <^F.o2,F.o1^> <> {} by A1,FUNCTOR0:def 19;
  hence thesis by A3,ALTCAT_3:6;
end;

theorem
  for A, B being category, F being contravariant Functor of A, B for o1,
  o2 being object of A st o1, o2 are_iso holds F.o2, F.o1 are_iso
proof
  let A, B be category, F be contravariant Functor of A, B, o1, o2 be object
  of A;
  assume
A1: o1, o2 are_iso;
  then consider a being Morphism of o1, o2 such that
A2: a is iso by ALTCAT_3:def 6;
A3: <^o1,o2^> <> {} & <^o2,o1^> <> {} by A1,ALTCAT_3:def 6;
  hence <^F.o2,F.o1^> <> {} & <^F.o1,F.o2^> <> {} by FUNCTOR0:def 19;
  take F.a;
  thus thesis by A3,A2,Th24;
end;

theorem Th26:
  for A, B being transitive with_units non empty AltCatStr for F
being covariant Functor of A, B for o1, o2 being object of A, a being Morphism
  of o1, o2 st F is full faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F.a is
  retraction holds a is retraction
proof
  let A, B be transitive with_units non empty AltCatStr, F be covariant
  Functor of A, B, o1, o2 be object of A, a be Morphism of o1, o2 such that
A1: F is full faithful and
A2: <^o1,o2^> <> {} and
A3: <^o2,o1^> <> {};
A4: <^F.o2,F.o1^> <> {} by A3,FUNCTOR0:def 18;
  assume F.a is retraction;
  then consider b being Morphism of F.o2, F.o1 such that
A5: b is_right_inverse_of F.a by ALTCAT_3:def 2;
  Morph-Map(F,o2,o1) is onto by A1,FUNCTOR1:15;
  then rng Morph-Map(F,o2,o1) = <^F.o2,F.o1^> by FUNCT_2:def 3;
  then consider a9 being set such that
A6: a9 in dom Morph-Map(F,o2,o1) and
A7: b = Morph-Map(F,o2,o1).a9 by A4,FUNCT_1:def 3;
  reconsider a9 as Morphism of o2, o1 by A4,A6,FUNCT_2:def 1;
  take a9;
A8: (F.a) * b = idm F.o2 by A5,ALTCAT_3:def 1;
A9: dom Morph-Map(F,o2,o2) = <^o2,o2^> & Morph-Map(F,o2,o2) is one-to-one
  by A1,FUNCTOR1:16,FUNCT_2:def 1;
  Morph-Map(F,o2,o2).idm o2 = F.(idm o2) by FUNCTOR0:def 15
    .= idm F.o2 by FUNCTOR2:1
    .= (F.a) * F.a9 by A3,A8,A4,A7,FUNCTOR0:def 15
    .= F.(a * a9) by A2,A3,FUNCTOR0:def 23
    .= Morph-Map(F,o2,o2).(a * a9) by FUNCTOR0:def 15;
  hence a * a9 = idm o2 by A9,FUNCT_1:def 4;
end;

theorem Th27:
  for A, B being transitive with_units non empty AltCatStr for F
being covariant Functor of A, B for o1, o2 being object of A, a being Morphism
  of o1, o2 st F is full faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F.a is
  coretraction holds a is coretraction
proof
  let A, B be transitive with_units non empty AltCatStr, F be covariant
  Functor of A, B, o1, o2 be object of A, a be Morphism of o1, o2 such that
A1: F is full faithful and
A2: <^o1,o2^> <> {} and
A3: <^o2,o1^> <> {};
A4: <^F.o2,F.o1^> <> {} by A3,FUNCTOR0:def 18;
  assume F.a is coretraction;
  then consider b being Morphism of F.o2, F.o1 such that
A5: F.a is_right_inverse_of b by ALTCAT_3:def 3;
  Morph-Map(F,o2,o1) is onto by A1,FUNCTOR1:15;
  then rng Morph-Map(F,o2,o1) = <^F.o2,F.o1^> by FUNCT_2:def 3;
  then consider a9 being set such that
A6: a9 in dom Morph-Map(F,o2,o1) and
A7: b = Morph-Map(F,o2,o1).a9 by A4,FUNCT_1:def 3;
  reconsider a9 as Morphism of o2, o1 by A4,A6,FUNCT_2:def 1;
  take a9;
A8: b * (F.a) = idm F.o1 by A5,ALTCAT_3:def 1;
A9: dom Morph-Map(F,o1,o1) = <^o1,o1^> & Morph-Map(F,o1,o1) is one-to-one
  by A1,FUNCTOR1:16,FUNCT_2:def 1;
  Morph-Map(F,o1,o1).idm o1 = F.(idm o1) by FUNCTOR0:def 15
    .= idm F.o1 by FUNCTOR2:1
    .= (F.a9) * F.a by A3,A8,A4,A7,FUNCTOR0:def 15
    .= F.(a9 * a) by A2,A3,FUNCTOR0:def 23
    .= Morph-Map(F,o1,o1).(a9 * a) by FUNCTOR0:def 15;
  hence a9 * a = idm o1 by A9,FUNCT_1:def 4;
end;

theorem Th28:
  for A, B being category, F being covariant Functor of A, B for
o1, o2 being object of A, a being Morphism of o1, o2 st F is full faithful & <^
  o1,o2^> <> {} & <^o2,o1^> <> {} & F.a is iso holds a is iso
proof
  let A, B be category, F be covariant Functor of A, B, o1, o2 be object of A,
  a be Morphism of o1, o2 such that
A1: F is full faithful and
A2: <^o1,o2^> <> {} & <^o2,o1^> <> {} and
A3: F.a is iso;
  <^F.o1,F.o2^> <> {} & <^F.o2,F.o1^> <> {} by A2,FUNCTOR0:def 18;
  then F.a is retraction coretraction by A3,ALTCAT_3:6;
  then a is retraction coretraction by A1,A2,Th26,Th27;
  hence thesis by A2,ALTCAT_3:6;
end;

theorem
  for A, B being category, F being covariant Functor of A, B for o1, o2
being object of A st F is full faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F
  .o1, F.o2 are_iso holds o1, o2 are_iso
proof
  let A, B be category, F be covariant Functor of A, B, o1, o2 be object of A
  such that
A1: F is full faithful and
A2: <^o1,o2^> <> {} and
A3: <^o2,o1^> <> {} and
A4: F.o1, F.o2 are_iso;
  consider Fa being Morphism of F.o1, F.o2 such that
A5: Fa is iso by A4,ALTCAT_3:def 6;
  consider a being Morphism of o1, o2 such that
A6: Fa = F.a by A1,A2,Th16;
  thus <^o1,o2^> <> {} & <^o2,o1^> <> {} by A2,A3;
  take a;
  thus thesis by A1,A2,A3,A5,A6,Th28;
end;

theorem Th30:
  for A, B being transitive with_units non empty AltCatStr for F
  being contravariant Functor of A, B for o1, o2 being object of A, a being
Morphism of o1, o2 st F is full faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} &
  F.a is retraction holds a is coretraction
proof
  let A, B be transitive with_units non empty AltCatStr, F be contravariant
  Functor of A, B, o1, o2 be object of A, a be Morphism of o1, o2 such that
A1: F is full faithful and
A2: <^o1,o2^> <> {} and
A3: <^o2,o1^> <> {};
A4: <^F.o1,F.o2^> <> {} by A3,FUNCTOR0:def 19;
  assume F.a is retraction;
  then consider b being Morphism of F.o1, F.o2 such that
A5: b is_right_inverse_of F.a by ALTCAT_3:def 2;
  Morph-Map(F,o2,o1) is onto by A1,Th14;
  then rng Morph-Map(F,o2,o1) = <^F.o1,F.o2^> by FUNCT_2:def 3;
  then consider a9 being set such that
A6: a9 in dom Morph-Map(F,o2,o1) and
A7: b = Morph-Map(F,o2,o1).a9 by A4,FUNCT_1:def 3;
  reconsider a9 as Morphism of o2, o1 by A4,A6,FUNCT_2:def 1;
  take a9;
A8: (F.a) * b = idm F.o1 by A5,ALTCAT_3:def 1;
A9: dom Morph-Map(F,o1,o1) = <^o1,o1^> & Morph-Map(F,o1,o1) is one-to-one
  by A1,Th15,FUNCT_2:def 1;
  Morph-Map(F,o1,o1).idm o1 = F.(idm o1) by FUNCTOR0:def 16
    .= idm F.o1 by Th13
    .= (F.a) * F.a9 by A3,A8,A4,A7,FUNCTOR0:def 16
    .= F.(a9 * a) by A2,A3,FUNCTOR0:def 24
    .= Morph-Map(F,o1,o1).(a9 * a) by FUNCTOR0:def 16;
  hence a9 * a = idm o1 by A9,FUNCT_1:def 4;
end;

theorem Th31:
  for A, B being transitive with_units non empty AltCatStr for F
  being contravariant Functor of A, B for o1, o2 being object of A, a being
Morphism of o1, o2 st F is full faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} &
  F.a is coretraction holds a is retraction
proof
  let A, B be transitive with_units non empty AltCatStr, F be contravariant
  Functor of A, B, o1, o2 be object of A, a be Morphism of o1, o2 such that
A1: F is full faithful and
A2: <^o1,o2^> <> {} and
A3: <^o2,o1^> <> {};
A4: <^F.o1,F.o2^> <> {} by A3,FUNCTOR0:def 19;
  assume F.a is coretraction;
  then consider b being Morphism of F.o1, F.o2 such that
A5: F.a is_right_inverse_of b by ALTCAT_3:def 3;
  Morph-Map(F,o2,o1) is onto by A1,Th14;
  then rng Morph-Map(F,o2,o1) = <^F.o1,F.o2^> by FUNCT_2:def 3;
  then consider a9 being set such that
A6: a9 in dom Morph-Map(F,o2,o1) and
A7: b = Morph-Map(F,o2,o1).a9 by A4,FUNCT_1:def 3;
  reconsider a9 as Morphism of o2, o1 by A4,A6,FUNCT_2:def 1;
  take a9;
A8: b * (F.a) = idm F.o2 by A5,ALTCAT_3:def 1;
A9: dom Morph-Map(F,o2,o2) = <^o2,o2^> & Morph-Map(F,o2,o2) is one-to-one
  by A1,Th15,FUNCT_2:def 1;
  Morph-Map(F,o2,o2).idm o2 = F.(idm o2) by FUNCTOR0:def 16
    .= idm F.o2 by Th13
    .= (F.a9) * F.a by A3,A8,A4,A7,FUNCTOR0:def 16
    .= F.(a * a9) by A2,A3,FUNCTOR0:def 24
    .= Morph-Map(F,o2,o2).(a * a9) by FUNCTOR0:def 16;
  hence a * a9 = idm o2 by A9,FUNCT_1:def 4;
end;

theorem Th32:
  for A, B being category, F being contravariant Functor of A, B
for o1, o2 being object of A, a being Morphism of o1, o2 st F is full faithful
  & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F.a is iso holds a is iso
proof
  let A, B be category, F be contravariant Functor of A, B, o1, o2 be object
  of A, a be Morphism of o1, o2 such that
A1: F is full faithful and
A2: <^o1,o2^> <> {} & <^o2,o1^> <> {} and
A3: F.a is iso;
  <^F.o1,F.o2^> <> {} & <^F.o2,F.o1^> <> {} by A2,FUNCTOR0:def 19;
  then F.a is retraction coretraction by A3,ALTCAT_3:6;
  then a is retraction coretraction by A1,A2,Th30,Th31;
  hence thesis by A2,ALTCAT_3:6;
end;

theorem
  for A, B being category, F being contravariant Functor of A, B for o1,
o2 being object of A st F is full faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {}
  & F.o2, F.o1 are_iso holds o1, o2 are_iso
proof
  let A, B be category, F be contravariant Functor of A, B, o1, o2 be object
  of A such that
A1: F is full faithful and
A2: <^o1,o2^> <> {} and
A3: <^o2,o1^> <> {} and
A4: F.o2, F.o1 are_iso;
  consider Fa being Morphism of F.o2, F.o1 such that
A5: Fa is iso by A4,ALTCAT_3:def 6;
  consider a being Morphism of o1, o2 such that
A6: Fa = F.a by A1,A2,Th17;
  thus <^o1,o2^> <> {} & <^o2,o1^> <> {} by A2,A3;
  take a;
  thus thesis by A1,A2,A3,A5,A6,Th32;
end;

Lm1: now
  let C be non empty transitive AltCatStr, p1, p2, p3 be object of C such that
A1: (the Arrows of C).(p1,p3) = {};
  thus [:(the Arrows of C).(p2,p3),(the Arrows of C).(p1,p2):] = {}
  proof
    assume [:(the Arrows of C).(p2,p3),(the Arrows of C).(p1,p2):] <> {};
    then consider k being set such that
A2: k in [:(the Arrows of C).(p2,p3),(the Arrows of C).(p1,p2):] by
XBOOLE_0:def 1;
    consider u1, u2 being set such that
A3: u1 in (the Arrows of C).(p2,p3) & u2 in (the Arrows of C).(p1,p2) and
    k = [u1,u2] by A2,ZFMISC_1:def 2;
    u1 in <^p2,p3^> & u2 in <^p1,p2^> by A3;
    then <^p1,p3^> <> {} by ALTCAT_1:def 2;
    hence contradiction by A1;
  end;
end;

begin  :: The subcategories of the morphisms

theorem Th34:
  for C being AltCatStr, D being SubCatStr of C st the carrier of
  C = the carrier of D & the Arrows of C = the Arrows of D holds D is full
proof
  let C be AltCatStr, D be SubCatStr of C;
  assume that
A1: the carrier of C = the carrier of D and
A2: the Arrows of C = the Arrows of D;
  dom (the Arrows of C) = [:the carrier of D, the carrier of D:] by A1,
PARTFUN1:def 2;
  hence the Arrows of D = (the Arrows of C)||the carrier of D by A2,RELAT_1:68;
end;

theorem Th35:
  for C being with_units non empty AltCatStr, D being SubCatStr
of C st the carrier of C = the carrier of D & the Arrows of C = the Arrows of D
  holds D is id-inheriting
proof
  let C be with_units non empty AltCatStr, D be SubCatStr of C;
  assume
  the carrier of C = the carrier of D & the Arrows of C = the Arrows of D;
  then reconsider D as full non empty SubCatStr of C by Th34;
  now
    let o be object of D, o9 be object of C;
    assume o = o9;
    then <^o9,o9^> = <^o,o^> by ALTCAT_2:28;
    hence idm o9 in <^o,o^>;
  end;
  hence thesis by ALTCAT_2:def 14;
end;

registration
  let C be category;
  cluster full non empty strict for subcategory of C;
  existence
  proof
    reconsider D = the AltCatStr of C as SubCatStr of C by ALTCAT_2:def 11;
    reconsider D as full non empty id-inheriting SubCatStr of C by Th34,Th35;
    take D;
    thus thesis;
  end;
end;

theorem Th36:
  for B being non empty subcategory of C for A being non empty
  subcategory of B holds A is non empty subcategory of C
proof
  let B be non empty subcategory of C, A be non empty subcategory of B;
  reconsider D = A as with_units non empty SubCatStr of C by ALTCAT_2:21;
  now
    let o be object of D, o1 be object of C such that
A1: o = o1;
    o in the carrier of D & the carrier of D c= the carrier of B by
ALTCAT_2:def 11;
    then reconsider oo = o as object of B;
    idm o = idm oo by ALTCAT_2:34
      .= idm o1 by A1,ALTCAT_2:34;
    hence idm o1 in <^o,o^>;
  end;
  hence thesis by ALTCAT_2:def 14;
end;

theorem Th37:
  for C being non empty transitive AltCatStr for D being non empty
transitive SubCatStr of C for o1, o2 being object of C, p1, p2 being object of
D for m being Morphism of o1, o2, n being Morphism of p1, p2 st p1 = o1 & p2 =
  o2 & m = n & <^p1,p2^> <> {} holds (m is mono implies n is mono) & (m is epi
  implies n is epi)
proof
  let C be non empty transitive AltCatStr, D be non empty transitive SubCatStr
of C, o1, o2 be object of C, p1, p2 be object of D, m be Morphism of o1, o2, n
  be Morphism of p1, p2 such that
A1: p1 = o1 and
A2: p2 = o2 and
A3: m = n & <^p1,p2^> <> {};
  thus m is mono implies n is mono
  proof
    assume
A4: m is mono;
    let p3 be object of D such that
A5: <^p3,p1^> <> {};
    reconsider o3 = p3 as object of C by ALTCAT_2:29;
A6: <^o3,o1^> <> {} by A1,A5,ALTCAT_2:31,XBOOLE_1:3;
    let f, g be Morphism of p3, p1 such that
A7: n * f = n * g;
    reconsider f1 = f, g1 = g as Morphism of o3, o1 by A1,A5,ALTCAT_2:33;
    m * f1 = n * f by A1,A2,A3,A5,ALTCAT_2:32
      .= m * g1 by A1,A2,A3,A5,A7,ALTCAT_2:32;
    hence thesis by A4,A6,ALTCAT_3:def 7;
  end;
  assume
A8: m is epi;
  let p3 be object of D such that
A9: <^p2,p3^> <> {};
  reconsider o3 = p3 as object of C by ALTCAT_2:29;
A10: <^o2,o3^> <> {} by A2,A9,ALTCAT_2:31,XBOOLE_1:3;
  let f, g be Morphism of p2, p3 such that
A11: f * n = g * n;
  reconsider f1 = f, g1 = g as Morphism of o2, o3 by A2,A9,ALTCAT_2:33;
  f1 * m = f * n by A1,A2,A3,A9,ALTCAT_2:32
    .= g1 * m by A1,A2,A3,A9,A11,ALTCAT_2:32;
  hence thesis by A8,A10,ALTCAT_3:def 8;
end;

theorem Th38:
  for D being non empty subcategory of C for o1, o2 being object
  of C, p1, p2 being object of D for m being Morphism of o1, o2, m1 being
Morphism of o2, o1 for n being Morphism of p1, p2, n1 being Morphism of p2, p1
  st p1 = o1 & p2 = o2 & m = n & m1 = n1 & <^p1,p2^> <> {} & <^p2,p1^> <> {}
  holds (m is_left_inverse_of m1 iff n is_left_inverse_of n1) & (m
  is_right_inverse_of m1 iff n is_right_inverse_of n1)
proof
  let D be non empty subcategory of C, o1, o2 be object of C, p1, p2 be object
  of D, m be Morphism of o1, o2, m1 be Morphism of o2, o1, n be Morphism of p1,
  p2, n1 be Morphism of p2, p1 such that
A1: p1 = o1 and
A2: p2 = o2 and
A3: m = n & m1 = n1 & <^p1,p2^> <> {} & <^p2,p1^> <> {};
  thus m is_left_inverse_of m1 iff n is_left_inverse_of n1
  proof
    thus m is_left_inverse_of m1 implies n is_left_inverse_of n1
    proof
      assume
A4:   m is_left_inverse_of m1;
      thus n * n1 = m * m1 by A1,A2,A3,ALTCAT_2:32
        .= idm o2 by A4,ALTCAT_3:def 1
        .= idm p2 by A2,ALTCAT_2:34;
    end;
    assume
A5: n is_left_inverse_of n1;
    thus m * m1 = n * n1 by A1,A2,A3,ALTCAT_2:32
      .= idm p2 by A5,ALTCAT_3:def 1
      .= idm o2 by A2,ALTCAT_2:34;
  end;
  thus m is_right_inverse_of m1 implies n is_right_inverse_of n1
  proof
    assume
A6: m is_right_inverse_of m1;
    thus n1 * n = m1 * m by A1,A2,A3,ALTCAT_2:32
      .= idm o1 by A6,ALTCAT_3:def 1
      .= idm p1 by A1,ALTCAT_2:34;
  end;
  assume
A7: n is_right_inverse_of n1;
  thus m1 * m = n1 * n by A1,A2,A3,ALTCAT_2:32
    .= idm p1 by A7,ALTCAT_3:def 1
    .= idm o1 by A1,ALTCAT_2:34;
end;

theorem
  for D being full non empty subcategory of C for o1, o2 being object of
C, p1, p2 being object of D for m being Morphism of o1, o2, n being Morphism of
p1, p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} & <^p2,p1^> <> {} holds (
  m is retraction implies n is retraction) & (m is coretraction implies n is
  coretraction) & (m is iso implies n is iso)
proof
  let D be full non empty subcategory of C, o1, o2 be object of C, p1, p2 be
  object of D, m be Morphism of o1, o2, n be Morphism of p1, p2;
  assume that
A1: p1 = o1 & p2 = o2 and
A2: m = n and
A3: <^p1,p2^> <> {} & <^p2,p1^> <> {};
  thus
A4: m is retraction implies n is retraction
  proof
    assume m is retraction;
    then consider B being Morphism of o2, o1 such that
A5: B is_right_inverse_of m by ALTCAT_3:def 2;
    reconsider B1 = B as Morphism of p2, p1 by A1,ALTCAT_2:28;
    take B1;
    thus thesis by A1,A2,A3,A5,Th38;
  end;
  thus
A6: m is coretraction implies n is coretraction
  proof
    assume m is coretraction;
    then consider B being Morphism of o2, o1 such that
A7: B is_left_inverse_of m by ALTCAT_3:def 3;
    reconsider B1 = B as Morphism of p2, p1 by A1,ALTCAT_2:28;
    take B1;
    thus thesis by A1,A2,A3,A7,Th38;
  end;
  assume m is iso;
  hence thesis by A3,A4,A6,ALTCAT_3:5,6;
end;

theorem Th40:
  for D being non empty subcategory of C for o1, o2 being object
of C, p1, p2 being object of D for m being Morphism of o1, o2, n being Morphism
  of p1, p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} & <^p2,p1^> <> {}
holds (n is retraction implies m is retraction) & (n is coretraction implies m
  is coretraction) & (n is iso implies m is iso)
proof
  let D be non empty subcategory of C, o1, o2 be object of C, p1, p2 be object
  of D, m be Morphism of o1, o2, n be Morphism of p1, p2 such that
A1: p1 = o1 & p2 = o2 and
A2: m = n and
A3: <^p1,p2^> <> {} and
A4: <^p2,p1^> <> {};
A5: <^o1,o2^> <> {} & <^o2,o1^> <> {} by A1,A3,A4,ALTCAT_2:31,XBOOLE_1:3;
  thus
A6: n is retraction implies m is retraction
  proof
    assume n is retraction;
    then consider B being Morphism of p2, p1 such that
A7: B is_right_inverse_of n by ALTCAT_3:def 2;
    reconsider B1 = B as Morphism of o2, o1 by A1,A4,ALTCAT_2:33;
    take B1;
    thus thesis by A1,A2,A3,A4,A7,Th38;
  end;
  thus
A8: n is coretraction implies m is coretraction
  proof
    assume n is coretraction;
    then consider B being Morphism of p2, p1 such that
A9: B is_left_inverse_of n by ALTCAT_3:def 3;
    reconsider B1 = B as Morphism of o2, o1 by A1,A4,ALTCAT_2:33;
    take B1;
    thus thesis by A1,A2,A3,A4,A9,Th38;
  end;
  assume n is iso;
  hence thesis by A6,A8,A5,ALTCAT_3:5,6;
end;

definition
  let C be category;
  func AllMono C -> strict non empty transitive SubCatStr of C means
  :Def1:
  the carrier of it = the carrier of C & the Arrows of it cc= the Arrows of C &
for o1, o2 being object of C, m being Morphism of o1, o2 holds m in (the Arrows
  of it).(o1,o2) iff <^o1,o2^> <> {} & m is mono;
  existence
  proof
    defpred P[set,set] means for x being set holds x in $2 iff ex o1, o2 being
object of C, m being Morphism of o1, o2 st $1 = [o1,o2] & <^o1,o2^> <> {} & x =
    m & m is mono;
    set I = the carrier of C;
A1: for i being set st i in [:I,I:] ex X being set st P[i,X]
    proof
      let i be set;
      assume i in [:I,I:];
      then consider o1, o2 being set such that
A2:   o1 in I & o2 in I and
A3:   i = [o1,o2] by ZFMISC_1:84;
      reconsider o1, o2 as object of C by A2;
      defpred P[set] means ex m being Morphism of o1, o2 st <^o1,o2^> <> {} &
      m = $1 & m is mono;
      consider X being set such that
A4:   for x being set holds x in X iff x in (the Arrows of C).(o1,o2)
      & P[x] from XBOOLE_0:sch 1;
      take X;
      let x be set;
      thus x in X implies ex o1, o2 being object of C, m being Morphism of o1,
      o2 st i = [o1,o2] & <^o1,o2^> <> {} & x = m & m is mono
      proof
        assume x in X;
        then consider m being Morphism of o1, o2 such that
A5:     <^o1,o2^> <> {} & m = x & m is mono by A4;
        take o1, o2, m;
        thus thesis by A3,A5;
      end;
      given p1, p2 being object of C, m being Morphism of p1, p2 such that
A6:   i = [p1,p2] and
A7:   <^p1,p2^> <> {} & x = m & m is mono;
      o1 = p1 & o2 = p2 by A3,A6,XTUPLE_0:1;
      hence thesis by A4,A7;
    end;
    consider Ar being ManySortedSet of [:I,I:] such that
A8: for i being set st i in [:I,I:] holds P[i,Ar.i] from PBOOLE:sch 3
    (A1);
    defpred R[set,set] means ex p1, p2, p3 being object of C st $1 = [p1,p2,p3
    ] & $2 = ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):] qua set);
A9: for i being set st i in [:I,I,I:] ex j being set st R[i,j]
    proof
      let i be set;
      assume i in [:I,I,I:];
      then consider p1, p2, p3 being set such that
A10:  p1 in I & p2 in I & p3 in I and
A11:  i = [p1,p2,p3] by MCART_1:68;
      reconsider p1, p2, p3 as object of C by A10;
      take ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):] qua set);
      take p1, p2, p3;
      thus i = [p1,p2,p3] by A11;
      thus thesis;
    end;
    consider Co being ManySortedSet of [:I,I,I:] such that
A12: for i being set st i in [:I,I,I:] holds R[i,Co.i] from PBOOLE:sch
    3 (A9 );
A13: Ar cc= the Arrows of C
    proof
      thus [:I,I:] c= [:the carrier of C,the carrier of C:];
      let i be set;
      assume
A14:  i in [:I,I:];
      let q be set;
      assume q in Ar.i;
      then
      ex p1, p2 being object of C, m being Morphism of p1, p2 st i = [p1,
      p2] & <^p1,p2^> <> {} & q = m & m is mono by A8,A14;
      hence thesis;
    end;
    Co is ManySortedFunction of {|Ar,Ar|}, {|Ar|}
    proof
      let i be set;
      assume i in [:I,I,I:];
      then consider p1, p2, p3 being object of C such that
A15:  i = [p1,p2,p3] and
A16:  Co.i = ((the Comp of C).(p1,p2,p3))| ([:Ar.(p2,p3),Ar.(p1,p2):]
      qua set) by A12;
A17:  [p1,p2] in [:I,I:] by ZFMISC_1:def 2;
      then
A18:  Ar.[p1,p2] c= (the Arrows of C).(p1,p2) by A13,ALTCAT_2:def 2;
A19:  [p2,p3] in [:I,I:] by ZFMISC_1:def 2;
      then Ar.[p2,p3] c= (the Arrows of C).(p2,p3) by A13,ALTCAT_2:def 2;
      then
A20:  [:Ar.(p2,p3),Ar.(p1,p2):] c= [:(the Arrows of C).(p2,p3),(the
      Arrows of C).(p1,p2):] by A18,ZFMISC_1:96;
      (the Arrows of C).(p1,p3) = {} implies [:(the Arrows of C).(p2,p3),
      (the Arrows of C).(p1,p2):] = {} by Lm1;
      then reconsider f = Co.i as Function of [:Ar.(p2,p3),Ar.(p1,p2):], (the
      Arrows of C).(p1,p3) by A16,A20,FUNCT_2:32;
A21:  Ar.[p1,p2] c= (the Arrows of C).[p1,p2] by A13,A17,ALTCAT_2:def 2;
A22:  Ar.[p2,p3] c= (the Arrows of C).[p2,p3] by A13,A19,ALTCAT_2:def 2;
A23:  (the Arrows of C).(p1,p3) = {} implies [:Ar.(p2,p3),Ar.(p1,p2):] = {}
      proof
        assume
A24:    (the Arrows of C).(p1,p3) = {};
        assume [:Ar.(p2,p3),Ar.(p1,p2):] <> {};
        then consider k being set such that
A25:    k in [:Ar.(p2,p3),Ar.(p1,p2):] by XBOOLE_0:def 1;
        consider u1, u2 being set such that
A26:    u1 in Ar.(p2,p3) & u2 in Ar.(p1,p2) and
        k = [u1,u2] by A25,ZFMISC_1:def 2;
        u1 in <^p2,p3^> & u2 in <^p1,p2^> by A22,A21,A26;
        then <^p1,p3^> <> {} by ALTCAT_1:def 2;
        hence contradiction by A24;
      end;
A27:  {|Ar|}.(p1,p2,p3) = Ar.(p1,p3) by ALTCAT_1:def 3;
A28:  rng f c= {|Ar|}.i
      proof
        let q be set;
        assume q in rng f;
        then consider x being set such that
A29:    x in dom f and
A30:    q = f.x by FUNCT_1:def 3;
A31:    dom f = [:Ar.(p2,p3),Ar.(p1,p2):] by A23,FUNCT_2:def 1;
        then consider m1, m2 being set such that
A32:    m1 in Ar.(p2,p3) and
A33:    m2 in Ar.(p1,p2) and
A34:    x = [m1,m2] by A29,ZFMISC_1:84;
        [p2,p3] in [:I,I:] by ZFMISC_1:def 2;
        then consider
        q2, q3 being object of C, qq being Morphism of q2, q3 such
        that
A35:    [p2,p3] = [q2,q3] and
A36:    <^q2,q3^> <> {} and
A37:    m1 = qq and
A38:    qq is mono by A8,A32;
        [p1,p2] in [:I,I:] by ZFMISC_1:def 2;
        then consider
        r1, r2 being object of C, rr being Morphism of r1, r2 such
        that
A39:    [p1,p2] = [r1,r2] and
A40:    <^r1,r2^> <> {} and
A41:    m2 = rr and
A42:    rr is mono by A8,A33;
A43:    ex o1, o3 being object of C, m being Morphism of o1, o3 st [p1,p3
        ] = [o1,o3] & <^o1,o3^> <> {} & q = m & m is mono
        proof
A44:      p2 = q2 by A35,XTUPLE_0:1;
          then reconsider mm = qq as Morphism of r2, q3 by A39,XTUPLE_0:1;
          take r1, q3, mm * rr;
A45:      p1 = r1 by A39,XTUPLE_0:1;
          hence [p1,p3] = [r1,q3] by A35,XTUPLE_0:1;
A46:      r2 = p2 by A39,XTUPLE_0:1;
          hence <^r1,q3^> <> {} by A36,A40,A44,ALTCAT_1:def 2;
A47:      p3 = q3 by A35,XTUPLE_0:1;
          thus q = (the Comp of C).(p1,p2,p3).(mm,rr) by A16,A29,A30,A31,A34
,A37,A41,FUNCT_1:49
            .= mm * rr by A35,A36,A40,A46,A45,A47,ALTCAT_1:def 8;
          thus thesis by A36,A38,A40,A42,A46,A44,ALTCAT_3:9;
        end;
        [p1,p3] in [:I,I:] by ZFMISC_1:def 2;
        then q in Ar.[p1,p3] by A8,A43;
        hence thesis by A15,A27,MULTOP_1:def 1;
      end;
      {|Ar,Ar|}.(p1,p2,p3) = [:Ar.(p2,p3),Ar.(p1,p2):] by ALTCAT_1:def 4;
      then [:Ar.(p2,p3),Ar.(p1,p2):] = {|Ar,Ar|}.i by A15,MULTOP_1:def 1;
      hence thesis by A23,A28,FUNCT_2:6;
    end;
    then reconsider Co as BinComp of Ar;
    set IT = AltCatStr (#I, Ar, Co#), J = the carrier of IT;
    IT is SubCatStr of C
    proof
      thus the carrier of IT c= the carrier of C;
      thus the Arrows of IT cc= the Arrows of C by A13;
      thus [:J,J,J:] c= [:I,I,I:];
      let i be set;
      assume i in [:J,J,J:];
      then consider p1, p2, p3 being object of C such that
A48:  i = [p1,p2,p3] and
A49:  Co.i = ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):]
      qua set) by A12;
A50:  ((the Comp of C).(p1,p2,p3)) qua Relation |([:Ar.(p2,p3),Ar.(p1,p2)
      :] qua set) c= (the Comp of C).(p1,p2,p3) by RELAT_1:59;
      let q be set;
      assume q in (the Comp of IT).i;
      then q in (the Comp of C).(p1,p2,p3) by A49,A50;
      hence thesis by A48,MULTOP_1:def 1;
    end;
    then reconsider IT as strict non empty SubCatStr of C;
    IT is transitive
    proof
      let p1, p2, p3 be object of IT;
      assume that
A51:  <^p1,p2^> <> {} and
A52:  <^p2,p3^> <> {};
      consider m2 being set such that
A53:  m2 in <^p1,p2^> by A51,XBOOLE_0:def 1;
      consider m1 being set such that
A54:  m1 in <^p2,p3^> by A52,XBOOLE_0:def 1;
      [p2,p3] in [:I,I:] by ZFMISC_1:def 2;
      then consider
      q2, q3 being object of C, qq being Morphism of q2, q3 such that
A55:  [p2,p3] = [q2,q3] and
A56:  <^q2,q3^> <> {} and
      m1 = qq and
A57:  qq is mono by A8,A54;
      [p1,p2] in [:I,I:] by ZFMISC_1:def 2;
      then consider
      r1, r2 being object of C, rr being Morphism of r1, r2 such that
A58:  [p1,p2] = [r1,r2] and
A59:  <^r1,r2^> <> {} and
      m2 = rr and
A60:  rr is mono by A8,A53;
A61:  p2 = q2 by A55,XTUPLE_0:1;
      then reconsider mm = qq as Morphism of r2, q3 by A58,XTUPLE_0:1;
A62:  r2 = p2 by A58,XTUPLE_0:1;
A63:  ex o1, o3 being object of C, m being Morphism of o1, o3 st [p1,p3]
      = [o1,o3] & <^o1,o3^> <> {} & mm * rr = m & m is mono
      proof
        take r1, q3, mm * rr;
        p1 = r1 by A58,XTUPLE_0:1;
        hence [p1,p3] = [r1,q3] by A55,XTUPLE_0:1;
        thus <^r1,q3^> <> {} by A56,A59,A62,A61,ALTCAT_1:def 2;
        thus mm * rr = mm * rr;
        thus thesis by A56,A57,A59,A60,A62,A61,ALTCAT_3:9;
      end;
      [p1,p3] in [:I,I:] by ZFMISC_1:def 2;
      hence thesis by A8,A63;
    end;
    then reconsider IT as strict non empty transitive SubCatStr of C;
    take IT;
    thus the carrier of IT = the carrier of C;
    thus the Arrows of IT cc= the Arrows of C by A13;
    let o1, o2 be object of C, m be Morphism of o1, o2;
A64: [o1,o2] in [:I,I:] by ZFMISC_1:def 2;
    thus m in (the Arrows of IT).(o1,o2) implies <^o1,o2^> <> {} & m is mono
    proof
      assume m in (the Arrows of IT).(o1,o2);
      then consider
      p1, p2 being object of C, n being Morphism of p1, p2 such that
A65:  [o1,o2] = [p1,p2] and
A66:  <^p1,p2^> <> {} & m = n & n is mono by A8,A64;
      o1 = p1 & o2 = p2 by A65,XTUPLE_0:1;
      hence thesis by A66;
    end;
    assume <^o1,o2^> <> {} & m is mono;
    hence thesis by A8,A64;
  end;
  uniqueness
  proof
    let S1, S2 be strict non empty transitive SubCatStr of C such that
A67: the carrier of S1 = the carrier of C and
A68: the Arrows of S1 cc= the Arrows of C and
A69: for o1, o2 being object of C, m being Morphism of o1, o2 holds m
    in (the Arrows of S1).(o1,o2) iff <^o1,o2^> <> {} & m is mono and
A70: the carrier of S2 = the carrier of C and
A71: the Arrows of S2 cc= the Arrows of C and
A72: for o1, o2 being object of C, m being Morphism of o1, o2 holds m
    in (the Arrows of S2).(o1,o2) iff <^o1,o2^> <> {} & m is mono;
    now
      let i be set;
      assume
A73:  i in [:the carrier of C,the carrier of C:];
      then consider o1, o2 being set such that
A74:  o1 in the carrier of C & o2 in the carrier of C and
A75:  i = [o1,o2] by ZFMISC_1:84;
      reconsider o1, o2 as object of C by A74;
      thus (the Arrows of S1).i = (the Arrows of S2).i
      proof
        thus (the Arrows of S1).i c= (the Arrows of S2).i
        proof
          let n be set such that
A76:      n in (the Arrows of S1).i;
          (the Arrows of S1).i c= (the Arrows of C).i by A67,A68,A73,
ALTCAT_2:def 2;
          then reconsider m = n as Morphism of o1, o2 by A75,A76;
          m in (the Arrows of S1).(o1,o2) by A75,A76;
          then <^o1,o2^> <> {} & m is mono by A69;
          then m in (the Arrows of S2).(o1,o2) by A72;
          hence thesis by A75;
        end;
        let n be set such that
A77:    n in (the Arrows of S2).i;
        (the Arrows of S2).i c= (the Arrows of C).i by A70,A71,A73,
ALTCAT_2:def 2;
        then reconsider m = n as Morphism of o1, o2 by A75,A77;
        m in (the Arrows of S2).(o1,o2) by A75,A77;
        then <^o1,o2^> <> {} & m is mono by A72;
        then m in (the Arrows of S1).(o1,o2) by A69;
        hence thesis by A75;
      end;
    end;
    hence thesis by A67,A70,ALTCAT_2:26,PBOOLE:3;
  end;
end;

registration
  let C be category;
  cluster AllMono C -> id-inheriting;
  coherence
  proof
    for o be object of AllMono C, o9 be object of C st o = o9 holds idm o9
    in <^o,o^> by Def1;
    hence thesis by ALTCAT_2:def 14;
  end;
end;

definition
  let C be category;
  func AllEpi C -> strict non empty transitive SubCatStr of C means
  :Def2:
  the
  carrier of it = the carrier of C & the Arrows of it cc= the Arrows of C & for
o1, o2 being object of C, m being Morphism of o1, o2 holds m in (the Arrows of
  it).(o1,o2) iff <^o1,o2^> <> {} & m is epi;
  existence
  proof
    defpred P[set,set] means for x being set holds x in $2 iff ex o1, o2 being
object of C, m being Morphism of o1, o2 st $1 = [o1,o2] & <^o1,o2^> <> {} & x =
    m & m is epi;
    set I = the carrier of C;
A1: for i being set st i in [:I,I:] ex X being set st P[i,X]
    proof
      let i be set;
      assume i in [:I,I:];
      then consider o1, o2 being set such that
A2:   o1 in I & o2 in I and
A3:   i = [o1,o2] by ZFMISC_1:84;
      reconsider o1, o2 as object of C by A2;
      defpred P[set] means ex m being Morphism of o1, o2 st <^o1,o2^> <> {} &
      m = $1 & m is epi;
      consider X being set such that
A4:   for x being set holds x in X iff x in (the Arrows of C).(o1,o2)
      & P[x] from XBOOLE_0:sch 1;
      take X;
      let x be set;
      thus x in X implies ex o1, o2 being object of C, m being Morphism of o1,
      o2 st i = [o1,o2] & <^o1,o2^> <> {} & x = m & m is epi
      proof
        assume x in X;
        then consider m being Morphism of o1, o2 such that
A5:     <^o1,o2^> <> {} & m = x & m is epi by A4;
        take o1, o2, m;
        thus thesis by A3,A5;
      end;
      given p1, p2 being object of C, m being Morphism of p1, p2 such that
A6:   i = [p1,p2] and
A7:   <^p1,p2^> <> {} & x = m & m is epi;
      o1 = p1 & o2 = p2 by A3,A6,XTUPLE_0:1;
      hence thesis by A4,A7;
    end;
    consider Ar being ManySortedSet of [:I,I:] such that
A8: for i being set st i in [:I,I:] holds P[i,Ar.i] from PBOOLE:sch 3
    (A1);
    defpred R[set,set] means ex p1, p2, p3 being object of C st $1 = [p1,p2,p3
    ] & $2 = ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):] qua set);
A9: for i being set st i in [:I,I,I:] ex j being set st R[i,j]
    proof
      let i be set;
      assume i in [:I,I,I:];
      then consider p1, p2, p3 being set such that
A10:  p1 in I & p2 in I & p3 in I and
A11:  i = [p1,p2,p3] by MCART_1:68;
      reconsider p1, p2, p3 as object of C by A10;
      take ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):] qua set);
      take p1, p2, p3;
      thus i = [p1,p2,p3] by A11;
      thus thesis;
    end;
    consider Co being ManySortedSet of [:I,I,I:] such that
A12: for i being set st i in [:I,I,I:] holds R[i,Co.i] from PBOOLE:sch
    3 (A9 );
A13: Ar cc= the Arrows of C
    proof
      thus [:I,I:] c= [:the carrier of C,the carrier of C:];
      let i be set;
      assume
A14:  i in [:I,I:];
      let q be set;
      assume q in Ar.i;
      then
      ex p1, p2 being object of C, m being Morphism of p1, p2 st i = [p1,
      p2] & <^p1,p2^> <> {} & q = m & m is epi by A8,A14;
      hence thesis;
    end;
    Co is ManySortedFunction of {|Ar,Ar|}, {|Ar|}
    proof
      let i be set;
      assume i in [:I,I,I:];
      then consider p1, p2, p3 being object of C such that
A15:  i = [p1,p2,p3] and
A16:  Co.i = ((the Comp of C).(p1,p2,p3))| ([:Ar.(p2,p3),Ar.(p1,p2):]
      qua set) by A12;
A17:  [p1,p2] in [:I,I:] by ZFMISC_1:def 2;
      then
A18:  Ar.[p1,p2] c= (the Arrows of C).(p1,p2) by A13,ALTCAT_2:def 2;
A19:  [p2,p3] in [:I,I:] by ZFMISC_1:def 2;
      then Ar.[p2,p3] c= (the Arrows of C).(p2,p3) by A13,ALTCAT_2:def 2;
      then
A20:  [:Ar.(p2,p3),Ar.(p1,p2):] c= [:(the Arrows of C).(p2,p3),(the
      Arrows of C).(p1,p2):] by A18,ZFMISC_1:96;
      (the Arrows of C).(p1,p3) = {} implies [:(the Arrows of C).(p2,p3),
      (the Arrows of C).(p1,p2):] = {} by Lm1;
      then reconsider f = Co.i as Function of [:Ar.(p2,p3),Ar.(p1,p2):], (the
      Arrows of C).(p1,p3) by A16,A20,FUNCT_2:32;
A21:  Ar.[p1,p2] c= (the Arrows of C).[p1,p2] by A13,A17,ALTCAT_2:def 2;
A22:  Ar.[p2,p3] c= (the Arrows of C).[p2,p3] by A13,A19,ALTCAT_2:def 2;
A23:  (the Arrows of C).(p1,p3) = {} implies [:Ar.(p2,p3),Ar.(p1,p2):] = {}
      proof
        assume
A24:    (the Arrows of C).(p1,p3) = {};
        assume [:Ar.(p2,p3),Ar.(p1,p2):] <> {};
        then consider k being set such that
A25:    k in [:Ar.(p2,p3),Ar.(p1,p2):] by XBOOLE_0:def 1;
        consider u1, u2 being set such that
A26:    u1 in Ar.(p2,p3) & u2 in Ar.(p1,p2) and
        k = [u1,u2] by A25,ZFMISC_1:def 2;
        u1 in <^p2,p3^> & u2 in <^p1,p2^> by A22,A21,A26;
        then <^p1,p3^> <> {} by ALTCAT_1:def 2;
        hence contradiction by A24;
      end;
A27:  {|Ar|}.(p1,p2,p3) = Ar.(p1,p3) by ALTCAT_1:def 3;
A28:  rng f c= {|Ar|}.i
      proof
        let q be set;
        assume q in rng f;
        then consider x being set such that
A29:    x in dom f and
A30:    q = f.x by FUNCT_1:def 3;
A31:    dom f = [:Ar.(p2,p3),Ar.(p1,p2):] by A23,FUNCT_2:def 1;
        then consider m1, m2 being set such that
A32:    m1 in Ar.(p2,p3) and
A33:    m2 in Ar.(p1,p2) and
A34:    x = [m1,m2] by A29,ZFMISC_1:84;
        [p2,p3] in [:I,I:] by ZFMISC_1:def 2;
        then consider
        q2, q3 being object of C, qq being Morphism of q2, q3 such
        that
A35:    [p2,p3] = [q2,q3] and
A36:    <^q2,q3^> <> {} and
A37:    m1 = qq and
A38:    qq is epi by A8,A32;
        [p1,p2] in [:I,I:] by ZFMISC_1:def 2;
        then consider
        r1, r2 being object of C, rr being Morphism of r1, r2 such
        that
A39:    [p1,p2] = [r1,r2] and
A40:    <^r1,r2^> <> {} and
A41:    m2 = rr and
A42:    rr is epi by A8,A33;
A43:    ex o1, o3 being object of C, m being Morphism of o1, o3 st [p1,p3
        ] = [o1,o3] & <^o1,o3^> <> {} & q = m & m is epi
        proof
A44:      p2 = q2 by A35,XTUPLE_0:1;
          then reconsider mm = qq as Morphism of r2, q3 by A39,XTUPLE_0:1;
          take r1, q3, mm * rr;
A45:      p1 = r1 by A39,XTUPLE_0:1;
          hence [p1,p3] = [r1,q3] by A35,XTUPLE_0:1;
A46:      r2 = p2 by A39,XTUPLE_0:1;
          hence <^r1,q3^> <> {} by A36,A40,A44,ALTCAT_1:def 2;
A47:      p3 = q3 by A35,XTUPLE_0:1;
          thus q = (the Comp of C).(p1,p2,p3).(mm,rr) by A16,A29,A30,A31,A34
,A37,A41,FUNCT_1:49
            .= mm * rr by A35,A36,A40,A46,A45,A47,ALTCAT_1:def 8;
          thus thesis by A36,A38,A40,A42,A46,A44,ALTCAT_3:10;
        end;
        [p1,p3] in [:I,I:] by ZFMISC_1:def 2;
        then q in Ar.[p1,p3] by A8,A43;
        hence thesis by A15,A27,MULTOP_1:def 1;
      end;
      {|Ar,Ar|}.(p1,p2,p3) = [:Ar.(p2,p3),Ar.(p1,p2):] by ALTCAT_1:def 4;
      then [:Ar.(p2,p3),Ar.(p1,p2):] = {|Ar,Ar|}.i by A15,MULTOP_1:def 1;
      hence thesis by A23,A28,FUNCT_2:6;
    end;
    then reconsider Co as BinComp of Ar;
    set IT = AltCatStr (#I, Ar, Co#), J = the carrier of IT;
    IT is SubCatStr of C
    proof
      thus the carrier of IT c= the carrier of C;
      thus the Arrows of IT cc= the Arrows of C by A13;
      thus [:J,J,J:] c= [:I,I,I:];
      let i be set;
      assume i in [:J,J,J:];
      then consider p1, p2, p3 being object of C such that
A48:  i = [p1,p2,p3] and
A49:  Co.i = ((the Comp of C).(p1,p2,p3))| ([:Ar.(p2,p3),Ar.(p1,p2):]
      qua set) by A12;
A50:  ((the Comp of C).(p1,p2,p3))| ([:Ar.(p2,p3),Ar.(p1,p2):] qua set)
      c= (the Comp of C).(p1,p2,p3) by RELAT_1:59;
      let q be set;
      assume q in (the Comp of IT).i;
      then q in (the Comp of C).(p1,p2,p3) by A49,A50;
      hence thesis by A48,MULTOP_1:def 1;
    end;
    then reconsider IT as strict non empty SubCatStr of C;
    IT is transitive
    proof
      let p1, p2, p3 be object of IT;
      assume that
A51:  <^p1,p2^> <> {} and
A52:  <^p2,p3^> <> {};
      consider m2 being set such that
A53:  m2 in <^p1,p2^> by A51,XBOOLE_0:def 1;
      consider m1 being set such that
A54:  m1 in <^p2,p3^> by A52,XBOOLE_0:def 1;
      [p2,p3] in [:I,I:] by ZFMISC_1:def 2;
      then consider
      q2, q3 being object of C, qq being Morphism of q2, q3 such that
A55:  [p2,p3] = [q2,q3] and
A56:  <^q2,q3^> <> {} and
      m1 = qq and
A57:  qq is epi by A8,A54;
      [p1,p2] in [:I,I:] by ZFMISC_1:def 2;
      then consider
      r1, r2 being object of C, rr being Morphism of r1, r2 such that
A58:  [p1,p2] = [r1,r2] and
A59:  <^r1,r2^> <> {} and
      m2 = rr and
A60:  rr is epi by A8,A53;
A61:  p2 = q2 by A55,XTUPLE_0:1;
      then reconsider mm = qq as Morphism of r2, q3 by A58,XTUPLE_0:1;
A62:  r2 = p2 by A58,XTUPLE_0:1;
A63:  ex o1, o3 being object of C, m being Morphism of o1, o3 st [p1,p3]
      = [o1,o3] & <^o1,o3^> <> {} & mm * rr = m & m is epi
      proof
        take r1, q3, mm * rr;
        p1 = r1 by A58,XTUPLE_0:1;
        hence [p1,p3] = [r1,q3] by A55,XTUPLE_0:1;
        thus <^r1,q3^> <> {} by A56,A59,A62,A61,ALTCAT_1:def 2;
        thus mm * rr = mm * rr;
        thus thesis by A56,A57,A59,A60,A62,A61,ALTCAT_3:10;
      end;
      [p1,p3] in [:I,I:] by ZFMISC_1:def 2;
      hence thesis by A8,A63;
    end;
    then reconsider IT as strict non empty transitive SubCatStr of C;
    take IT;
    thus the carrier of IT = the carrier of C;
    thus the Arrows of IT cc= the Arrows of C by A13;
    let o1, o2 be object of C, m be Morphism of o1, o2;
A64: [o1,o2] in [:I,I:] by ZFMISC_1:def 2;
    thus m in (the Arrows of IT).(o1,o2) implies <^o1,o2^> <> {} & m is epi
    proof
      assume m in (the Arrows of IT).(o1,o2);
      then consider
      p1, p2 being object of C, n being Morphism of p1, p2 such that
A65:  [o1,o2] = [p1,p2] and
A66:  <^p1,p2^> <> {} & m = n & n is epi by A8,A64;
      o1 = p1 & o2 = p2 by A65,XTUPLE_0:1;
      hence thesis by A66;
    end;
    assume <^o1,o2^> <> {} & m is epi;
    hence thesis by A8,A64;
  end;
  uniqueness
  proof
    let S1, S2 be strict non empty transitive SubCatStr of C such that
A67: the carrier of S1 = the carrier of C and
A68: the Arrows of S1 cc= the Arrows of C and
A69: for o1, o2 being object of C, m being Morphism of o1, o2 holds m
    in (the Arrows of S1).(o1,o2) iff <^o1,o2^> <> {} & m is epi and
A70: the carrier of S2 = the carrier of C and
A71: the Arrows of S2 cc= the Arrows of C and
A72: for o1, o2 being object of C, m being Morphism of o1, o2 holds m
    in (the Arrows of S2).(o1,o2) iff <^o1,o2^> <> {} & m is epi;
    now
      let i be set;
      assume
A73:  i in [:the carrier of C,the carrier of C:];
      then consider o1, o2 being set such that
A74:  o1 in the carrier of C & o2 in the carrier of C and
A75:  i = [o1,o2] by ZFMISC_1:84;
      reconsider o1, o2 as object of C by A74;
      thus (the Arrows of S1).i = (the Arrows of S2).i
      proof
        thus (the Arrows of S1).i c= (the Arrows of S2).i
        proof
          let n be set such that
A76:      n in (the Arrows of S1).i;
          (the Arrows of S1).i c= (the Arrows of C).i by A67,A68,A73,
ALTCAT_2:def 2;
          then reconsider m = n as Morphism of o1, o2 by A75,A76;
          m in (the Arrows of S1).(o1,o2) by A75,A76;
          then <^o1,o2^> <> {} & m is epi by A69;
          then m in (the Arrows of S2).(o1,o2) by A72;
          hence thesis by A75;
        end;
        let n be set such that
A77:    n in (the Arrows of S2).i;
        (the Arrows of S2).i c= (the Arrows of C).i by A70,A71,A73,
ALTCAT_2:def 2;
        then reconsider m = n as Morphism of o1, o2 by A75,A77;
        m in (the Arrows of S2).(o1,o2) by A75,A77;
        then <^o1,o2^> <> {} & m is epi by A72;
        then m in (the Arrows of S1).(o1,o2) by A69;
        hence thesis by A75;
      end;
    end;
    hence thesis by A67,A70,ALTCAT_2:26,PBOOLE:3;
  end;
end;

registration
  let C be category;
  cluster AllEpi C -> id-inheriting;
  coherence
  proof
    for o be object of AllEpi C, o9 be object of C st o = o9 holds idm o9
    in <^o,o^> by Def2;
    hence thesis by ALTCAT_2:def 14;
  end;
end;

definition
  let C be category;
  func AllRetr C -> strict non empty transitive SubCatStr of C means
  :Def3:
  the carrier of it = the carrier of C & the Arrows of it cc= the Arrows of C &
for o1, o2 being object of C, m being Morphism of o1, o2 holds m in (the Arrows
  of it).(o1,o2) iff <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction;
  existence
  proof
    defpred P[set,set] means for x being set holds x in $2 iff ex o1, o2 being
object of C, m being Morphism of o1, o2 st $1 = [o1,o2] & <^o1,o2^> <> {} & <^
    o2,o1^> <> {} & x = m & m is retraction;
    set I = the carrier of C;
A1: for i being set st i in [:I,I:] ex X being set st P[i,X]
    proof
      let i be set;
      assume i in [:I,I:];
      then consider o1, o2 being set such that
A2:   o1 in I & o2 in I and
A3:   i = [o1,o2] by ZFMISC_1:84;
      reconsider o1, o2 as object of C by A2;
      defpred P[set] means ex m being Morphism of o1, o2 st <^o1,o2^> <> {} &
      <^o2,o1^> <> {} & m = $1 & m is retraction;
      consider X being set such that
A4:   for x being set holds x in X iff x in (the Arrows of C).(o1,o2)
      & P[x] from XBOOLE_0:sch 1;
      take X;
      let x be set;
      thus x in X implies ex o1, o2 being object of C, m being Morphism of o1,
o2 st i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is retraction
      proof
        assume x in X;
        then consider m being Morphism of o1, o2 such that
A5:     <^o1,o2^> <> {} & <^o2,o1^> <> {} & m = x & m is retraction by A4;
        take o1, o2, m;
        thus thesis by A3,A5;
      end;
      given p1, p2 being object of C, m being Morphism of p1, p2 such that
A6:   i = [p1,p2] and
A7:   <^p1,p2^> <> {} & <^p2,p1^> <> {} & x = m & m is retraction;
      o1 = p1 & o2 = p2 by A3,A6,XTUPLE_0:1;
      hence thesis by A4,A7;
    end;
    consider Ar being ManySortedSet of [:I,I:] such that
A8: for i being set st i in [:I,I:] holds P[i,Ar.i] from PBOOLE:sch 3
    (A1);
    defpred R[set,set] means ex p1, p2, p3 being object of C st $1 = [p1,p2,p3
    ] & $2 = ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):] qua set);
A9: for i being set st i in [:I,I,I:] ex j being set st R[i,j]
    proof
      let i be set;
      assume i in [:I,I,I:];
      then consider p1, p2, p3 being set such that
A10:  p1 in I & p2 in I & p3 in I and
A11:  i = [p1,p2,p3] by MCART_1:68;
      reconsider p1, p2, p3 as object of C by A10;
      take ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):] qua set);
      take p1, p2, p3;
      thus i = [p1,p2,p3] by A11;
      thus thesis;
    end;
    consider Co being ManySortedSet of [:I,I,I:] such that
A12: for i being set st i in [:I,I,I:] holds R[i,Co.i] from PBOOLE:sch
    3 (A9 );
A13: Ar cc= the Arrows of C
    proof
      thus [:I,I:] c= [:the carrier of C,the carrier of C:];
      let i be set;
      assume
A14:  i in [:I,I:];
      let q be set;
      assume q in Ar.i;
      then
      ex p1, p2 being object of C, m being Morphism of p1, p2 st i = [p1,
p2] & <^p1,p2^> <> {} & <^p2,p1^> <> {} & q = m & m is retraction by A8,A14;
      hence thesis;
    end;
    Co is ManySortedFunction of {|Ar,Ar|}, {|Ar|}
    proof
      let i be set;
      assume i in [:I,I,I:];
      then consider p1, p2, p3 being object of C such that
A15:  i = [p1,p2,p3] and
A16:  Co.i = ((the Comp of C).(p1,p2,p3))| ([:Ar.(p2,p3),Ar.(p1,p2):]
      qua set) by A12;
A17:  [p1,p2] in [:I,I:] by ZFMISC_1:def 2;
      then
A18:  Ar.[p1,p2] c= (the Arrows of C).(p1,p2) by A13,ALTCAT_2:def 2;
A19:  [p2,p3] in [:I,I:] by ZFMISC_1:def 2;
      then Ar.[p2,p3] c= (the Arrows of C).(p2,p3) by A13,ALTCAT_2:def 2;
      then
A20:  [:Ar.(p2,p3),Ar.(p1,p2):] c= [:(the Arrows of C).(p2,p3),(the
      Arrows of C).(p1,p2):] by A18,ZFMISC_1:96;
      (the Arrows of C).(p1,p3) = {} implies [:(the Arrows of C).(p2,p3),
      (the Arrows of C).(p1,p2):] = {} by Lm1;
      then reconsider f = Co.i as Function of [:Ar.(p2,p3),Ar.(p1,p2):], (the
      Arrows of C).(p1,p3) by A16,A20,FUNCT_2:32;
A21:  Ar.[p1,p2] c= (the Arrows of C).[p1,p2] by A13,A17,ALTCAT_2:def 2;
A22:  Ar.[p2,p3] c= (the Arrows of C).[p2,p3] by A13,A19,ALTCAT_2:def 2;
A23:  (the Arrows of C).(p1,p3) = {} implies [:Ar.(p2,p3),Ar.(p1,p2):] = {}
      proof
        assume
A24:    (the Arrows of C).(p1,p3) = {};
        assume [:Ar.(p2,p3),Ar.(p1,p2):] <> {};
        then consider k being set such that
A25:    k in [:Ar.(p2,p3),Ar.(p1,p2):] by XBOOLE_0:def 1;
        consider u1, u2 being set such that
A26:    u1 in Ar.(p2,p3) & u2 in Ar.(p1,p2) and
        k = [u1,u2] by A25,ZFMISC_1:def 2;
        u1 in <^p2,p3^> & u2 in <^p1,p2^> by A22,A21,A26;
        then <^p1,p3^> <> {} by ALTCAT_1:def 2;
        hence contradiction by A24;
      end;
A27:  {|Ar|}.(p1,p2,p3) = Ar.(p1,p3) by ALTCAT_1:def 3;
A28:  rng f c= {|Ar|}.i
      proof
        let q be set;
        assume q in rng f;
        then consider x being set such that
A29:    x in dom f and
A30:    q = f.x by FUNCT_1:def 3;
A31:    dom f = [:Ar.(p2,p3),Ar.(p1,p2):] by A23,FUNCT_2:def 1;
        then consider m1, m2 being set such that
A32:    m1 in Ar.(p2,p3) and
A33:    m2 in Ar.(p1,p2) and
A34:    x = [m1,m2] by A29,ZFMISC_1:84;
        [p2,p3] in [:I,I:] by ZFMISC_1:def 2;
        then consider
        q2, q3 being object of C, qq being Morphism of q2, q3 such
        that
A35:    [p2,p3] = [q2,q3] and
A36:    <^q2,q3^> <> {} and
A37:    <^q3,q2^> <> {} and
A38:    m1 = qq and
A39:    qq is retraction by A8,A32;
        [p1,p2] in [:I,I:] by ZFMISC_1:def 2;
        then consider
        r1, r2 being object of C, rr being Morphism of r1, r2 such
        that
A40:    [p1,p2] = [r1,r2] and
A41:    <^r1,r2^> <> {} and
A42:    <^r2,r1^> <> {} and
A43:    m2 = rr and
A44:    rr is retraction by A8,A33;
A45:    ex o1, o3 being object of C, m being Morphism of o1, o3 st [p1,p3
] = [o1,o3] & <^o1,o3^> <> {} & <^o3,o1^> <> {} & q = m & m is retraction
        proof
A46:      p2 = q2 by A35,XTUPLE_0:1;
          then reconsider mm = qq as Morphism of r2, q3 by A40,XTUPLE_0:1;
          take r1, q3, mm * rr;
A47:      p1 = r1 by A40,XTUPLE_0:1;
          hence [p1,p3] = [r1,q3] by A35,XTUPLE_0:1;
A48:      r2 = p2 by A40,XTUPLE_0:1;
          hence
A49:      <^r1,q3^> <> {} & <^q3,r1^> <> {} by A36,A37,A41,A42,A46,
ALTCAT_1:def 2;
A50:      p3 = q3 by A35,XTUPLE_0:1;
          thus q = (the Comp of C).(p1,p2,p3).(mm,rr) by A16,A29,A30,A31,A34
,A38,A43,FUNCT_1:49
            .= mm * rr by A35,A36,A41,A48,A47,A50,ALTCAT_1:def 8;
          thus thesis by A36,A39,A41,A44,A48,A46,A49,ALTCAT_3:18;
        end;
        [p1,p3] in [:I,I:] by ZFMISC_1:def 2;
        then q in Ar.[p1,p3] by A8,A45;
        hence thesis by A15,A27,MULTOP_1:def 1;
      end;
      {|Ar,Ar|}.(p1,p2,p3) = [:Ar.(p2,p3),Ar.(p1,p2):] by ALTCAT_1:def 4;
      then [:Ar.(p2,p3),Ar.(p1,p2):] = {|Ar,Ar|}.i by A15,MULTOP_1:def 1;
      hence thesis by A23,A28,FUNCT_2:6;
    end;
    then reconsider Co as BinComp of Ar;
    set IT = AltCatStr (#I, Ar, Co#), J = the carrier of IT;
    IT is SubCatStr of C
    proof
      thus the carrier of IT c= the carrier of C;
      thus the Arrows of IT cc= the Arrows of C by A13;
      thus [:J,J,J:] c= [:I,I,I:];
      let i be set;
      assume i in [:J,J,J:];
      then consider p1, p2, p3 being object of C such that
A51:  i = [p1,p2,p3] and
A52:  Co.i = ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):]
      qua set) by A12;
A53:  ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):] qua set) c=
      (the Comp of C).(p1,p2,p3) by RELAT_1:59;
      let q be set;
      assume q in (the Comp of IT).i;
      then q in (the Comp of C).(p1,p2,p3) by A52,A53;
      hence thesis by A51,MULTOP_1:def 1;
    end;
    then reconsider IT as strict non empty SubCatStr of C;
    IT is transitive
    proof
      let p1, p2, p3 be object of IT;
      assume that
A54:  <^p1,p2^> <> {} and
A55:  <^p2,p3^> <> {};
      consider m2 being set such that
A56:  m2 in <^p1,p2^> by A54,XBOOLE_0:def 1;
      consider m1 being set such that
A57:  m1 in <^p2,p3^> by A55,XBOOLE_0:def 1;
      [p2,p3] in [:I,I:] by ZFMISC_1:def 2;
      then consider
      q2, q3 being object of C, qq being Morphism of q2, q3 such that
A58:  [p2,p3] = [q2,q3] and
A59:  <^q2,q3^> <> {} and
A60:  <^q3,q2^> <> {} and
      m1 = qq and
A61:  qq is retraction by A8,A57;
      [p1,p2] in [:I,I:] by ZFMISC_1:def 2;
      then consider
      r1, r2 being object of C, rr being Morphism of r1, r2 such that
A62:  [p1,p2] = [r1,r2] and
A63:  <^r1,r2^> <> {} and
A64:  <^r2,r1^> <> {} and
      m2 = rr and
A65:  rr is retraction by A8,A56;
A66:  p2 = q2 by A58,XTUPLE_0:1;
      then reconsider mm = qq as Morphism of r2, q3 by A62,XTUPLE_0:1;
A67:  r2 = p2 by A62,XTUPLE_0:1;
A68:  ex o1, o3 being object of C, m being Morphism of o1, o3 st [p1,p3]
= [o1,o3] & <^o1,o3^> <> {} & <^o3,o1^> <> {} & mm * rr = m & m is retraction
      proof
        take r1, q3, mm * rr;
        p1 = r1 by A62,XTUPLE_0:1;
        hence [p1,p3] = [r1,q3] by A58,XTUPLE_0:1;
        thus
A69:    <^r1,q3^> <> {} & <^q3,r1^> <> {} by A59,A60,A63,A64,A67,A66,
ALTCAT_1:def 2;
        thus mm * rr = mm * rr;
        thus thesis by A59,A61,A63,A65,A67,A66,A69,ALTCAT_3:18;
      end;
      [p1,p3] in [:I,I:] by ZFMISC_1:def 2;
      hence thesis by A8,A68;
    end;
    then reconsider IT as strict non empty transitive SubCatStr of C;
    take IT;
    thus the carrier of IT = the carrier of C;
    thus the Arrows of IT cc= the Arrows of C by A13;
    let o1, o2 be object of C, m be Morphism of o1, o2;
A70: [o1,o2] in [:I,I:] by ZFMISC_1:def 2;
    thus m in (the Arrows of IT).(o1,o2) implies <^o1,o2^> <> {} & <^o2,o1^>
    <> {} & m is retraction
    proof
      assume m in (the Arrows of IT).(o1,o2);
      then consider
      p1, p2 being object of C, n being Morphism of p1, p2 such that
A71:  [o1,o2] = [p1,p2] and
A72:  <^p1,p2^> <> {} & <^p2,p1^> <> {} & m = n & n is retraction by A8,A70;
      o1 = p1 & o2 = p2 by A71,XTUPLE_0:1;
      hence thesis by A72;
    end;
    assume <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction;
    hence thesis by A8,A70;
  end;
  uniqueness
  proof
    let S1, S2 be strict non empty transitive SubCatStr of C such that
A73: the carrier of S1 = the carrier of C and
A74: the Arrows of S1 cc= the Arrows of C and
A75: for o1, o2 being object of C, m being Morphism of o1, o2 holds m
    in (the Arrows of S1).(o1,o2) iff <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is
    retraction and
A76: the carrier of S2 = the carrier of C and
A77: the Arrows of S2 cc= the Arrows of C and
A78: for o1, o2 being object of C, m being Morphism of o1, o2 holds m
    in (the Arrows of S2).(o1,o2) iff <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is
    retraction;
    now
      let i be set;
      assume
A79:  i in [:the carrier of C,the carrier of C:];
      then consider o1, o2 being set such that
A80:  o1 in the carrier of C & o2 in the carrier of C and
A81:  i = [o1,o2] by ZFMISC_1:84;
      reconsider o1, o2 as object of C by A80;
      thus (the Arrows of S1).i = (the Arrows of S2).i
      proof
        thus (the Arrows of S1).i c= (the Arrows of S2).i
        proof
          let n be set such that
A82:      n in (the Arrows of S1).i;
          (the Arrows of S1).i c= (the Arrows of C).i by A73,A74,A79,
ALTCAT_2:def 2;
          then reconsider m = n as Morphism of o1, o2 by A81,A82;
A83:      m in (the Arrows of S1).(o1,o2) by A81,A82;
          then
A84:      m is retraction by A75;
          <^o1,o2^> <> {} & <^o2,o1^> <> {} by A75,A83;
          then m in (the Arrows of S2).(o1,o2) by A78,A84;
          hence thesis by A81;
        end;
        let n be set such that
A85:    n in (the Arrows of S2).i;
        (the Arrows of S2).i c= (the Arrows of C).i by A76,A77,A79,
ALTCAT_2:def 2;
        then reconsider m = n as Morphism of o1, o2 by A81,A85;
A86:    m in (the Arrows of S2).(o1,o2) by A81,A85;
        then
A87:    m is retraction by A78;
        <^o1,o2^> <> {} & <^o2,o1^> <> {} by A78,A86;
        then m in (the Arrows of S1).(o1,o2) by A75,A87;
        hence thesis by A81;
      end;
    end;
    hence thesis by A73,A76,ALTCAT_2:26,PBOOLE:3;
  end;
end;

registration
  let C be category;
  cluster AllRetr C -> id-inheriting;
  coherence
  proof
    for o be object of AllRetr C, o9 be object of C st o = o9 holds idm o9
    in <^o,o^> by Def3;
    hence thesis by ALTCAT_2:def 14;
  end;
end;

definition
  let C be category;
  func AllCoretr C -> strict non empty transitive SubCatStr of C means
  :Def4:
  the carrier of it = the carrier of C & the Arrows of it cc= the Arrows of C &
for o1, o2 being object of C, m being Morphism of o1, o2 holds m in (the Arrows
  of it).(o1,o2) iff <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is coretraction;
  existence
  proof
    defpred P[set,set] means for x being set holds x in $2 iff ex o1, o2 being
object of C, m being Morphism of o1, o2 st $1 = [o1,o2] & <^o1,o2^> <> {} & <^
    o2,o1^> <> {} & x = m & m is coretraction;
    set I = the carrier of C;
A1: for i being set st i in [:I,I:] ex X being set st P[i,X]
    proof
      let i be set;
      assume i in [:I,I:];
      then consider o1, o2 being set such that
A2:   o1 in I & o2 in I and
A3:   i = [o1,o2] by ZFMISC_1:84;
      reconsider o1, o2 as object of C by A2;
      defpred P[set] means ex m being Morphism of o1, o2 st <^o1,o2^> <> {} &
      <^o2,o1^> <> {} & m = $1 & m is coretraction;
      consider X being set such that
A4:   for x being set holds x in X iff x in (the Arrows of C).(o1,o2)
      & P[x] from XBOOLE_0:sch 1;
      take X;
      let x be set;
      thus x in X implies ex o1, o2 being object of C, m being Morphism of o1,
      o2 st i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is
      coretraction
      proof
        assume x in X;
        then consider m being Morphism of o1, o2 such that
A5:     <^o1,o2^> <> {} & <^o2,o1^> <> {} & m = x & m is coretraction by A4;
        take o1, o2, m;
        thus thesis by A3,A5;
      end;
      given p1, p2 being object of C, m being Morphism of p1, p2 such that
A6:   i = [p1,p2] and
A7:   <^p1,p2^> <> {} & <^p2,p1^> <> {} & x = m & m is coretraction;
      o1 = p1 & o2 = p2 by A3,A6,XTUPLE_0:1;
      hence thesis by A4,A7;
    end;
    consider Ar being ManySortedSet of [:I,I:] such that
A8: for i being set st i in [:I,I:] holds P[i,Ar.i] from PBOOLE:sch 3
    (A1);
    defpred R[set,set] means ex p1, p2, p3 being object of C st $1 = [p1,p2,p3
    ] & $2 = ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):] qua set);
A9: for i being set st i in [:I,I,I:] ex j being set st R[i,j]
    proof
      let i be set;
      assume i in [:I,I,I:];
      then consider p1, p2, p3 being set such that
A10:  p1 in I & p2 in I & p3 in I and
A11:  i = [p1,p2,p3] by MCART_1:68;
      reconsider p1, p2, p3 as object of C by A10;
      take ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):] qua set);
      take p1, p2, p3;
      thus i = [p1,p2,p3] by A11;
      thus thesis;
    end;
    consider Co being ManySortedSet of [:I,I,I:] such that
A12: for i being set st i in [:I,I,I:] holds R[i,Co.i] from PBOOLE:sch
    3 (A9 );
A13: Ar cc= the Arrows of C
    proof
      thus [:I,I:] c= [:the carrier of C,the carrier of C:];
      let i be set;
      assume
A14:  i in [:I,I:];
      let q be set;
      assume q in Ar.i;
      then
      ex p1, p2 being object of C, m being Morphism of p1, p2 st i = [p1,
p2] & <^p1,p2^> <> {} & <^p2,p1^> <> {} & q = m & m is coretraction by A8,A14;
      hence thesis;
    end;
    Co is ManySortedFunction of {|Ar,Ar|}, {|Ar|}
    proof
      let i be set;
      assume i in [:I,I,I:];
      then consider p1, p2, p3 being object of C such that
A15:  i = [p1,p2,p3] and
A16:  Co.i = ((the Comp of C).(p1,p2,p3))| ([:Ar.(p2,p3),Ar.(p1,p2):]
      qua set) by A12;
A17:  [p1,p2] in [:I,I:] by ZFMISC_1:def 2;
      then
A18:  Ar.[p1,p2] c= (the Arrows of C).(p1,p2) by A13,ALTCAT_2:def 2;
A19:  [p2,p3] in [:I,I:] by ZFMISC_1:def 2;
      then Ar.[p2,p3] c= (the Arrows of C).(p2,p3) by A13,ALTCAT_2:def 2;
      then
A20:  [:Ar.(p2,p3),Ar.(p1,p2):] c= [:(the Arrows of C).(p2,p3),(the
      Arrows of C).(p1,p2):] by A18,ZFMISC_1:96;
      (the Arrows of C).(p1,p3) = {} implies [:(the Arrows of C).(p2,p3),
      (the Arrows of C).(p1,p2):] = {} by Lm1;
      then reconsider f = Co.i as Function of [:Ar.(p2,p3),Ar.(p1,p2):], (the
      Arrows of C).(p1,p3) by A16,A20,FUNCT_2:32;
A21:  Ar.[p1,p2] c= (the Arrows of C).[p1,p2] by A13,A17,ALTCAT_2:def 2;
A22:  Ar.[p2,p3] c= (the Arrows of C).[p2,p3] by A13,A19,ALTCAT_2:def 2;
A23:  (the Arrows of C).(p1,p3) = {} implies [:Ar.(p2,p3),Ar.(p1,p2):] = {}
      proof
        assume
A24:    (the Arrows of C).(p1,p3) = {};
        assume [:Ar.(p2,p3),Ar.(p1,p2):] <> {};
        then consider k being set such that
A25:    k in [:Ar.(p2,p3),Ar.(p1,p2):] by XBOOLE_0:def 1;
        consider u1, u2 being set such that
A26:    u1 in Ar.(p2,p3) & u2 in Ar.(p1,p2) and
        k = [u1,u2] by A25,ZFMISC_1:def 2;
        u1 in <^p2,p3^> & u2 in <^p1,p2^> by A22,A21,A26;
        then <^p1,p3^> <> {} by ALTCAT_1:def 2;
        hence contradiction by A24;
      end;
A27:  {|Ar|}.(p1,p2,p3) = Ar.(p1,p3) by ALTCAT_1:def 3;
A28:  rng f c= {|Ar|}.i
      proof
        let q be set;
        assume q in rng f;
        then consider x being set such that
A29:    x in dom f and
A30:    q = f.x by FUNCT_1:def 3;
A31:    dom f = [:Ar.(p2,p3),Ar.(p1,p2):] by A23,FUNCT_2:def 1;
        then consider m1, m2 being set such that
A32:    m1 in Ar.(p2,p3) and
A33:    m2 in Ar.(p1,p2) and
A34:    x = [m1,m2] by A29,ZFMISC_1:84;
        [p2,p3] in [:I,I:] by ZFMISC_1:def 2;
        then consider
        q2, q3 being object of C, qq being Morphism of q2, q3 such
        that
A35:    [p2,p3] = [q2,q3] and
A36:    <^q2,q3^> <> {} and
A37:    <^q3,q2^> <> {} and
A38:    m1 = qq and
A39:    qq is coretraction by A8,A32;
        [p1,p2] in [:I,I:] by ZFMISC_1:def 2;
        then consider
        r1, r2 being object of C, rr being Morphism of r1, r2 such
        that
A40:    [p1,p2] = [r1,r2] and
A41:    <^r1,r2^> <> {} and
A42:    <^r2,r1^> <> {} and
A43:    m2 = rr and
A44:    rr is coretraction by A8,A33;
A45:    ex o1, o3 being object of C, m being Morphism of o1, o3 st [p1,p3
] = [o1,o3] & <^o1,o3^> <> {} & <^o3,o1^> <> {} & q = m & m is coretraction
        proof
A46:      p2 = q2 by A35,XTUPLE_0:1;
          then reconsider mm = qq as Morphism of r2, q3 by A40,XTUPLE_0:1;
          take r1, q3, mm * rr;
A47:      p1 = r1 by A40,XTUPLE_0:1;
          hence [p1,p3] = [r1,q3] by A35,XTUPLE_0:1;
A48:      r2 = p2 by A40,XTUPLE_0:1;
          hence
A49:      <^r1,q3^> <> {} & <^q3,r1^> <> {} by A36,A37,A41,A42,A46,
ALTCAT_1:def 2;
A50:      p3 = q3 by A35,XTUPLE_0:1;
          thus q = (the Comp of C).(p1,p2,p3).(mm,rr) by A16,A29,A30,A31,A34
,A38,A43,FUNCT_1:49
            .= mm * rr by A35,A36,A41,A48,A47,A50,ALTCAT_1:def 8;
          thus thesis by A36,A39,A41,A44,A48,A46,A49,ALTCAT_3:19;
        end;
        [p1,p3] in [:I,I:] by ZFMISC_1:def 2;
        then q in Ar.[p1,p3] by A8,A45;
        hence thesis by A15,A27,MULTOP_1:def 1;
      end;
      {|Ar,Ar|}.(p1,p2,p3) = [:Ar.(p2,p3),Ar.(p1,p2):] by ALTCAT_1:def 4;
      then [:Ar.(p2,p3),Ar.(p1,p2):] = {|Ar,Ar|}.i by A15,MULTOP_1:def 1;
      hence thesis by A23,A28,FUNCT_2:6;
    end;
    then reconsider Co as BinComp of Ar;
    set IT = AltCatStr (#I, Ar, Co#), J = the carrier of IT;
    IT is SubCatStr of C
    proof
      thus the carrier of IT c= the carrier of C;
      thus the Arrows of IT cc= the Arrows of C by A13;
      thus [:J,J,J:] c= [:I,I,I:];
      let i be set;
      assume i in [:J,J,J:];
      then consider p1, p2, p3 being object of C such that
A51:  i = [p1,p2,p3] and
A52:  Co.i = ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):]
      qua set) by A12;
A53:  ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):] qua set) c=
      (the Comp of C).(p1,p2,p3) by RELAT_1:59;
      let q be set;
      assume q in (the Comp of IT).i;
      then q in (the Comp of C).(p1,p2,p3) by A52,A53;
      hence thesis by A51,MULTOP_1:def 1;
    end;
    then reconsider IT as strict non empty SubCatStr of C;
    IT is transitive
    proof
      let p1, p2, p3 be object of IT;
      assume that
A54:  <^p1,p2^> <> {} and
A55:  <^p2,p3^> <> {};
      consider m2 being set such that
A56:  m2 in <^p1,p2^> by A54,XBOOLE_0:def 1;
      consider m1 being set such that
A57:  m1 in <^p2,p3^> by A55,XBOOLE_0:def 1;
      [p2,p3] in [:I,I:] by ZFMISC_1:def 2;
      then consider
      q2, q3 being object of C, qq being Morphism of q2, q3 such that
A58:  [p2,p3] = [q2,q3] and
A59:  <^q2,q3^> <> {} and
A60:  <^q3,q2^> <> {} and
      m1 = qq and
A61:  qq is coretraction by A8,A57;
      [p1,p2] in [:I,I:] by ZFMISC_1:def 2;
      then consider
      r1, r2 being object of C, rr being Morphism of r1, r2 such that
A62:  [p1,p2] = [r1,r2] and
A63:  <^r1,r2^> <> {} and
A64:  <^r2,r1^> <> {} and
      m2 = rr and
A65:  rr is coretraction by A8,A56;
A66:  p2 = q2 by A58,XTUPLE_0:1;
      then reconsider mm = qq as Morphism of r2, q3 by A62,XTUPLE_0:1;
A67:  r2 = p2 by A62,XTUPLE_0:1;
A68:  ex o1, o3 being object of C, m being Morphism of o1, o3 st [p1,p3]
= [o1,o3] & <^o1,o3^> <> {} & <^o3,o1^> <> {} & mm * rr = m & m is coretraction
      proof
        take r1, q3, mm * rr;
        p1 = r1 by A62,XTUPLE_0:1;
        hence [p1,p3] = [r1,q3] by A58,XTUPLE_0:1;
        thus
A69:    <^r1,q3^> <> {} & <^q3,r1^> <> {} by A59,A60,A63,A64,A67,A66,
ALTCAT_1:def 2;
        thus mm * rr = mm * rr;
        thus thesis by A59,A61,A63,A65,A67,A66,A69,ALTCAT_3:19;
      end;
      [p1,p3] in [:I,I:] by ZFMISC_1:def 2;
      hence thesis by A8,A68;
    end;
    then reconsider IT as strict non empty transitive SubCatStr of C;
    take IT;
    thus the carrier of IT = the carrier of C;
    thus the Arrows of IT cc= the Arrows of C by A13;
    let o1, o2 be object of C, m be Morphism of o1, o2;
A70: [o1,o2] in [:I,I:] by ZFMISC_1:def 2;
    thus m in (the Arrows of IT).(o1,o2) implies <^o1,o2^> <> {} & <^o2,o1^>
    <> {} & m is coretraction
    proof
      assume m in (the Arrows of IT).(o1,o2);
      then consider
      p1, p2 being object of C, n being Morphism of p1, p2 such that
A71:  [o1,o2] = [p1,p2] and
A72:  <^p1,p2^> <> {} & <^p2,p1^> <> {} & m = n & n is coretraction by A8,A70;
      o1 = p1 & o2 = p2 by A71,XTUPLE_0:1;
      hence thesis by A72;
    end;
    assume <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is coretraction;
    hence thesis by A8,A70;
  end;
  uniqueness
  proof
    let S1, S2 be strict non empty transitive SubCatStr of C such that
A73: the carrier of S1 = the carrier of C and
A74: the Arrows of S1 cc= the Arrows of C and
A75: for o1, o2 being object of C, m being Morphism of o1, o2 holds m
    in (the Arrows of S1).(o1,o2) iff <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is
    coretraction and
A76: the carrier of S2 = the carrier of C and
A77: the Arrows of S2 cc= the Arrows of C and
A78: for o1, o2 being object of C, m being Morphism of o1, o2 holds m
    in (the Arrows of S2).(o1,o2) iff <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is
    coretraction;
    now
      let i be set;
      assume
A79:  i in [:the carrier of C,the carrier of C:];
      then consider o1, o2 being set such that
A80:  o1 in the carrier of C & o2 in the carrier of C and
A81:  i = [o1,o2] by ZFMISC_1:84;
      reconsider o1, o2 as object of C by A80;
      thus (the Arrows of S1).i = (the Arrows of S2).i
      proof
        thus (the Arrows of S1).i c= (the Arrows of S2).i
        proof
          let n be set such that
A82:      n in (the Arrows of S1).i;
          (the Arrows of S1).i c= (the Arrows of C).i by A73,A74,A79,
ALTCAT_2:def 2;
          then reconsider m = n as Morphism of o1, o2 by A81,A82;
A83:      m in (the Arrows of S1).(o1,o2) by A81,A82;
          then
A84:      m is coretraction by A75;
          <^o1,o2^> <> {} & <^o2,o1^> <> {} by A75,A83;
          then m in (the Arrows of S2).(o1,o2) by A78,A84;
          hence thesis by A81;
        end;
        let n be set such that
A85:    n in (the Arrows of S2).i;
        (the Arrows of S2).i c= (the Arrows of C).i by A76,A77,A79,
ALTCAT_2:def 2;
        then reconsider m = n as Morphism of o1, o2 by A81,A85;
A86:    m in (the Arrows of S2).(o1,o2) by A81,A85;
        then
A87:    m is coretraction by A78;
        <^o1,o2^> <> {} & <^o2,o1^> <> {} by A78,A86;
        then m in (the Arrows of S1).(o1,o2) by A75,A87;
        hence thesis by A81;
      end;
    end;
    hence thesis by A73,A76,ALTCAT_2:26,PBOOLE:3;
  end;
end;

registration
  let C be category;
  cluster AllCoretr C -> id-inheriting;
  coherence
  proof
    for o be object of AllCoretr C, o9 be object of C st o = o9 holds idm
    o9 in <^o,o^> by Def4;
    hence thesis by ALTCAT_2:def 14;
  end;
end;

definition
  let C be category;
  func AllIso C -> strict non empty transitive SubCatStr of C means
  :Def5:
  the
  carrier of it = the carrier of C & the Arrows of it cc= the Arrows of C & for
o1, o2 being object of C, m being Morphism of o1, o2 holds m in (the Arrows of
  it).(o1,o2) iff <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso;
  existence
  proof
    defpred P[set,set] means for x being set holds x in $2 iff ex o1, o2 being
object of C, m being Morphism of o1, o2 st $1 = [o1,o2] & <^o1,o2^> <> {} & <^
    o2,o1^> <> {} & x = m & m is iso;
    set I = the carrier of C;
A1: for i being set st i in [:I,I:] ex X being set st P[i,X]
    proof
      let i be set;
      assume i in [:I,I:];
      then consider o1, o2 being set such that
A2:   o1 in I & o2 in I and
A3:   i = [o1,o2] by ZFMISC_1:84;
      reconsider o1, o2 as object of C by A2;
      defpred P[set] means ex m being Morphism of o1, o2 st <^o1,o2^> <> {} &
      <^o2,o1^> <> {} & m = $1 & m is iso;
      consider X being set such that
A4:   for x being set holds x in X iff x in (the Arrows of C).(o1,o2)
      & P[x] from XBOOLE_0:sch 1;
      take X;
      let x be set;
      thus x in X implies ex o1, o2 being object of C, m being Morphism of o1,
      o2 st i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is iso
      proof
        assume x in X;
        then consider m being Morphism of o1, o2 such that
A5:     <^o1,o2^> <> {} & <^o2,o1^> <> {} & m = x & m is iso by A4;
        take o1, o2, m;
        thus thesis by A3,A5;
      end;
      given p1, p2 being object of C, m being Morphism of p1, p2 such that
A6:   i = [p1,p2] and
A7:   <^p1,p2^> <> {} & <^p2,p1^> <> {} & x = m & m is iso;
      o1 = p1 & o2 = p2 by A3,A6,XTUPLE_0:1;
      hence thesis by A4,A7;
    end;
    consider Ar being ManySortedSet of [:I,I:] such that
A8: for i being set st i in [:I,I:] holds P[i,Ar.i] from PBOOLE:sch 3
    (A1);
    defpred R[set,set] means ex p1, p2, p3 being object of C st $1 = [p1,p2,p3
    ] & $2 = ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):] qua set);
A9: for i being set st i in [:I,I,I:] ex j being set st R[i,j]
    proof
      let i be set;
      assume i in [:I,I,I:];
      then consider p1, p2, p3 being set such that
A10:  p1 in I & p2 in I & p3 in I and
A11:  i = [p1,p2,p3] by MCART_1:68;
      reconsider p1, p2, p3 as object of C by A10;
      take ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):] qua set);
      take p1, p2, p3;
      thus i = [p1,p2,p3] by A11;
      thus thesis;
    end;
    consider Co being ManySortedSet of [:I,I,I:] such that
A12: for i being set st i in [:I,I,I:] holds R[i,Co.i] from PBOOLE:sch
    3 (A9 );
A13: Ar cc= the Arrows of C
    proof
      thus [:I,I:] c= [:the carrier of C,the carrier of C:];
      let i be set;
      assume
A14:  i in [:I,I:];
      let q be set;
      assume q in Ar.i;
      then
      ex p1, p2 being object of C, m being Morphism of p1, p2 st i = [p1,
      p2] & <^p1,p2^> <> {} & <^p2,p1^> <> {} & q = m & m is iso by A8,A14;
      hence thesis;
    end;
    Co is ManySortedFunction of {|Ar,Ar|}, {|Ar|}
    proof
      let i be set;
      assume i in [:I,I,I:];
      then consider p1, p2, p3 being object of C such that
A15:  i = [p1,p2,p3] and
A16:  Co.i = ((the Comp of C).(p1,p2,p3))| ([:Ar.(p2,p3),Ar.(p1,p2):]
      qua set) by A12;
A17:  [p1,p2] in [:I,I:] by ZFMISC_1:def 2;
      then
A18:  Ar.[p1,p2] c= (the Arrows of C).(p1,p2) by A13,ALTCAT_2:def 2;
A19:  [p2,p3] in [:I,I:] by ZFMISC_1:def 2;
      then Ar.[p2,p3] c= (the Arrows of C).(p2,p3) by A13,ALTCAT_2:def 2;
      then
A20:  [:Ar.(p2,p3),Ar.(p1,p2):] c= [:(the Arrows of C).(p2,p3),(the
      Arrows of C).(p1,p2):] by A18,ZFMISC_1:96;
      (the Arrows of C).(p1,p3) = {} implies [:(the Arrows of C).(p2,p3),
      (the Arrows of C).(p1,p2):] = {} by Lm1;
      then reconsider f = Co.i as Function of [:Ar.(p2,p3),Ar.(p1,p2):], (the
      Arrows of C).(p1,p3) by A16,A20,FUNCT_2:32;
A21:  Ar.[p1,p2] c= (the Arrows of C).[p1,p2] by A13,A17,ALTCAT_2:def 2;
A22:  Ar.[p2,p3] c= (the Arrows of C).[p2,p3] by A13,A19,ALTCAT_2:def 2;
A23:  (the Arrows of C).(p1,p3) = {} implies [:Ar.(p2,p3),Ar.(p1,p2):] = {}
      proof
        assume
A24:    (the Arrows of C).(p1,p3) = {};
        assume [:Ar.(p2,p3),Ar.(p1,p2):] <> {};
        then consider k being set such that
A25:    k in [:Ar.(p2,p3),Ar.(p1,p2):] by XBOOLE_0:def 1;
        consider u1, u2 being set such that
A26:    u1 in Ar.(p2,p3) & u2 in Ar.(p1,p2) and
        k = [u1,u2] by A25,ZFMISC_1:def 2;
        u1 in <^p2,p3^> & u2 in <^p1,p2^> by A22,A21,A26;
        then <^p1,p3^> <> {} by ALTCAT_1:def 2;
        hence contradiction by A24;
      end;
A27:  {|Ar|}.(p1,p2,p3) = Ar.(p1,p3) by ALTCAT_1:def 3;
A28:  rng f c= {|Ar|}.i
      proof
        let q be set;
        assume q in rng f;
        then consider x being set such that
A29:    x in dom f and
A30:    q = f.x by FUNCT_1:def 3;
A31:    dom f = [:Ar.(p2,p3),Ar.(p1,p2):] by A23,FUNCT_2:def 1;
        then consider m1, m2 being set such that
A32:    m1 in Ar.(p2,p3) and
A33:    m2 in Ar.(p1,p2) and
A34:    x = [m1,m2] by A29,ZFMISC_1:84;
        [p2,p3] in [:I,I:] by ZFMISC_1:def 2;
        then consider
        q2, q3 being object of C, qq being Morphism of q2, q3 such
        that
A35:    [p2,p3] = [q2,q3] and
A36:    <^q2,q3^> <> {} and
A37:    <^q3,q2^> <> {} and
A38:    m1 = qq and
A39:    qq is iso by A8,A32;
        [p1,p2] in [:I,I:] by ZFMISC_1:def 2;
        then consider
        r1, r2 being object of C, rr being Morphism of r1, r2 such
        that
A40:    [p1,p2] = [r1,r2] and
A41:    <^r1,r2^> <> {} and
A42:    <^r2,r1^> <> {} and
A43:    m2 = rr and
A44:    rr is iso by A8,A33;
A45:    ex o1, o3 being object of C, m being Morphism of o1, o3 st [p1,p3
        ] = [o1,o3] & <^o1,o3^> <> {} & <^o3,o1^> <> {} & q = m & m is iso
        proof
A46:      p2 = q2 by A35,XTUPLE_0:1;
          then reconsider mm = qq as Morphism of r2, q3 by A40,XTUPLE_0:1;
          take r1, q3, mm * rr;
A47:      p1 = r1 by A40,XTUPLE_0:1;
          hence [p1,p3] = [r1,q3] by A35,XTUPLE_0:1;
A48:      r2 = p2 by A40,XTUPLE_0:1;
          hence
A49:      <^r1,q3^> <> {} & <^q3,r1^> <> {} by A36,A37,A41,A42,A46,
ALTCAT_1:def 2;
A50:      p3 = q3 by A35,XTUPLE_0:1;
          thus q = (the Comp of C).(p1,p2,p3).(mm,rr) by A16,A29,A30,A31,A34
,A38,A43,FUNCT_1:49
            .= mm * rr by A35,A36,A41,A48,A47,A50,ALTCAT_1:def 8;
          thus thesis by A36,A39,A41,A44,A48,A46,A49,ALTCAT_3:7;
        end;
        [p1,p3] in [:I,I:] by ZFMISC_1:def 2;
        then q in Ar.[p1,p3] by A8,A45;
        hence thesis by A15,A27,MULTOP_1:def 1;
      end;
      {|Ar,Ar|}.(p1,p2,p3) = [:Ar.(p2,p3),Ar.(p1,p2):] by ALTCAT_1:def 4;
      then [:Ar.(p2,p3),Ar.(p1,p2):] = {|Ar,Ar|}.i by A15,MULTOP_1:def 1;
      hence thesis by A23,A28,FUNCT_2:6;
    end;
    then reconsider Co as BinComp of Ar;
    set IT = AltCatStr (#I, Ar, Co#), J = the carrier of IT;
    IT is SubCatStr of C
    proof
      thus the carrier of IT c= the carrier of C;
      thus the Arrows of IT cc= the Arrows of C by A13;
      thus [:J,J,J:] c= [:I,I,I:];
      let i be set;
      assume i in [:J,J,J:];
      then consider p1, p2, p3 being object of C such that
A51:  i = [p1,p2,p3] and
A52:  Co.i = ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):]
      qua set) by A12;
A53:  ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):] qua set) c=
      (the Comp of C).(p1,p2,p3) by RELAT_1:59;
      let q be set;
      assume q in (the Comp of IT).i;
      then q in (the Comp of C).(p1,p2,p3) by A52,A53;
      hence thesis by A51,MULTOP_1:def 1;
    end;
    then reconsider IT as strict non empty SubCatStr of C;
    IT is transitive
    proof
      let p1, p2, p3 be object of IT;
      assume that
A54:  <^p1,p2^> <> {} and
A55:  <^p2,p3^> <> {};
      consider m2 being set such that
A56:  m2 in <^p1,p2^> by A54,XBOOLE_0:def 1;
      consider m1 being set such that
A57:  m1 in <^p2,p3^> by A55,XBOOLE_0:def 1;
      [p2,p3] in [:I,I:] by ZFMISC_1:def 2;
      then consider
      q2, q3 being object of C, qq being Morphism of q2, q3 such that
A58:  [p2,p3] = [q2,q3] and
A59:  <^q2,q3^> <> {} and
A60:  <^q3,q2^> <> {} and
      m1 = qq and
A61:  qq is iso by A8,A57;
      [p1,p2] in [:I,I:] by ZFMISC_1:def 2;
      then consider
      r1, r2 being object of C, rr being Morphism of r1, r2 such that
A62:  [p1,p2] = [r1,r2] and
A63:  <^r1,r2^> <> {} and
A64:  <^r2,r1^> <> {} and
      m2 = rr and
A65:  rr is iso by A8,A56;
A66:  p2 = q2 by A58,XTUPLE_0:1;
      then reconsider mm = qq as Morphism of r2, q3 by A62,XTUPLE_0:1;
A67:  r2 = p2 by A62,XTUPLE_0:1;
A68:  ex o1, o3 being object of C, m being Morphism of o1, o3 st [p1,p3]
      = [o1,o3] & <^o1,o3^> <> {} & <^o3,o1^> <> {} & mm * rr = m & m is iso
      proof
        take r1, q3, mm * rr;
        p1 = r1 by A62,XTUPLE_0:1;
        hence [p1,p3] = [r1,q3] by A58,XTUPLE_0:1;
        thus
A69:    <^r1,q3^> <> {} & <^q3,r1^> <> {} by A59,A60,A63,A64,A67,A66,
ALTCAT_1:def 2;
        thus mm * rr = mm * rr;
        thus thesis by A59,A61,A63,A65,A67,A66,A69,ALTCAT_3:7;
      end;
      [p1,p3] in [:I,I:] by ZFMISC_1:def 2;
      hence thesis by A8,A68;
    end;
    then reconsider IT as strict non empty transitive SubCatStr of C;
    take IT;
    thus the carrier of IT = the carrier of C;
    thus the Arrows of IT cc= the Arrows of C by A13;
    let o1, o2 be object of C, m be Morphism of o1, o2;
A70: [o1,o2] in [:I,I:] by ZFMISC_1:def 2;
    thus m in (the Arrows of IT).(o1,o2) implies <^o1,o2^> <> {} & <^o2,o1^>
    <> {} & m is iso
    proof
      assume m in (the Arrows of IT).(o1,o2);
      then consider
      p1, p2 being object of C, n being Morphism of p1, p2 such that
A71:  [o1,o2] = [p1,p2] and
A72:  <^p1,p2^> <> {} & <^p2,p1^> <> {} & m = n & n is iso by A8,A70;
      o1 = p1 & o2 = p2 by A71,XTUPLE_0:1;
      hence thesis by A72;
    end;
    assume <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso;
    hence thesis by A8,A70;
  end;
  uniqueness
  proof
    let S1, S2 be strict non empty transitive SubCatStr of C such that
A73: the carrier of S1 = the carrier of C and
A74: the Arrows of S1 cc= the Arrows of C and
A75: for o1, o2 being object of C, m being Morphism of o1, o2 holds m
in (the Arrows of S1).(o1,o2) iff <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso
    and
A76: the carrier of S2 = the carrier of C and
A77: the Arrows of S2 cc= the Arrows of C and
A78: for o1, o2 being object of C, m being Morphism of o1, o2 holds m
in (the Arrows of S2).(o1,o2) iff <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso;
    now
      let i be set;
      assume
A79:  i in [:the carrier of C,the carrier of C:];
      then consider o1, o2 being set such that
A80:  o1 in the carrier of C & o2 in the carrier of C and
A81:  i = [o1,o2] by ZFMISC_1:84;
      reconsider o1, o2 as object of C by A80;
      thus (the Arrows of S1).i = (the Arrows of S2).i
      proof
        thus (the Arrows of S1).i c= (the Arrows of S2).i
        proof
          let n be set such that
A82:      n in (the Arrows of S1).i;
          (the Arrows of S1).i c= (the Arrows of C).i by A73,A74,A79,
ALTCAT_2:def 2;
          then reconsider m = n as Morphism of o1, o2 by A81,A82;
A83:      m in (the Arrows of S1).(o1,o2) by A81,A82;
          then
A84:      m is iso by A75;
          <^o1,o2^> <> {} & <^o2,o1^> <> {} by A75,A83;
          then m in (the Arrows of S2).(o1,o2) by A78,A84;
          hence thesis by A81;
        end;
        let n be set such that
A85:    n in (the Arrows of S2).i;
        (the Arrows of S2).i c= (the Arrows of C).i by A76,A77,A79,
ALTCAT_2:def 2;
        then reconsider m = n as Morphism of o1, o2 by A81,A85;
A86:    m in (the Arrows of S2).(o1,o2) by A81,A85;
        then
A87:    m is iso by A78;
        <^o1,o2^> <> {} & <^o2,o1^> <> {} by A78,A86;
        then m in (the Arrows of S1).(o1,o2) by A75,A87;
        hence thesis by A81;
      end;
    end;
    hence thesis by A73,A76,ALTCAT_2:26,PBOOLE:3;
  end;
end;

registration
  let C be category;
  cluster AllIso C -> id-inheriting;
  coherence
  proof
    for o be object of AllIso C, o9 be object of C st o = o9 holds idm o9
    in <^o,o^> by Def5;
    hence thesis by ALTCAT_2:def 14;
  end;
end;

theorem Th41:
  AllIso C is non empty subcategory of AllRetr C
proof
  the carrier of AllIso C = the carrier of C by Def5;
  then
A1: the carrier of AllIso C c= the carrier of AllRetr C by Def3;
  the Arrows of AllIso C cc= the Arrows of AllRetr C
  proof
    thus [:the carrier of AllIso C,the carrier of AllIso C:] c= [:the carrier
    of AllRetr C,the carrier of AllRetr C:] by A1,ZFMISC_1:96;
    let i be set;
    assume
A2: i in [:the carrier of AllIso C,the carrier of AllIso C:];
    then consider o1, o2 being set such that
A3: o1 in the carrier of AllIso C & o2 in the carrier of AllIso C and
A4: i = [o1,o2] by ZFMISC_1:84;
    reconsider o1, o2 as object of C by A3,Def5;
    let m be set;
    assume
A5: m in (the Arrows of AllIso C).i;
    the Arrows of AllIso C cc= the Arrows of C by Def5;
    then
    (the Arrows of AllIso C).[o1,o2] c= (the Arrows of C).(o1,o2) by A2,A4,
ALTCAT_2:def 2;
    then reconsider m1 = m as Morphism of o1, o2 by A4,A5;
    m in (the Arrows of AllIso C).(o1,o2) by A4,A5;
    then m1 is iso by Def5;
    then
A6: m1 is retraction by ALTCAT_3:5;
    m1 in (the Arrows of AllIso C).(o1,o2) by A4,A5;
    then <^o1,o2^> <> {} & <^o2,o1^> <> {} by Def5;
    then m in (the Arrows of AllRetr C).(o1,o2) by A6,Def3;
    hence thesis by A4;
  end;
  then reconsider
  A = AllIso C as with_units non empty SubCatStr of AllRetr C by A1,ALTCAT_2:24
;
  now
    let o be object of A, o1 be object of AllRetr C such that
A7: o = o1;
    reconsider oo = o as object of C by Def5;
    idm o = idm oo by ALTCAT_2:34
      .= idm o1 by A7,ALTCAT_2:34;
    hence idm o1 in <^o,o^>;
  end;
  hence thesis by ALTCAT_2:def 14;
end;

theorem Th42:
  AllIso C is non empty subcategory of AllCoretr C
proof
  the carrier of AllIso C = the carrier of C by Def5;
  then
A1: the carrier of AllIso C c= the carrier of AllCoretr C by Def4;
  the Arrows of AllIso C cc= the Arrows of AllCoretr C
  proof
    thus [:the carrier of AllIso C,the carrier of AllIso C:] c= [:the carrier
    of AllCoretr C,the carrier of AllCoretr C:] by A1,ZFMISC_1:96;
    let i be set;
    assume
A2: i in [:the carrier of AllIso C,the carrier of AllIso C:];
    then consider o1, o2 being set such that
A3: o1 in the carrier of AllIso C & o2 in the carrier of AllIso C and
A4: i = [o1,o2] by ZFMISC_1:84;
    reconsider o1, o2 as object of C by A3,Def5;
    let m be set;
    assume
A5: m in (the Arrows of AllIso C).i;
    the Arrows of AllIso C cc= the Arrows of C by Def5;
    then
    (the Arrows of AllIso C).[o1,o2] c= (the Arrows of C).(o1,o2) by A2,A4,
ALTCAT_2:def 2;
    then reconsider m1 = m as Morphism of o1, o2 by A4,A5;
    m in (the Arrows of AllIso C).(o1,o2) by A4,A5;
    then m1 is iso by Def5;
    then
A6: m1 is coretraction by ALTCAT_3:5;
    m1 in (the Arrows of AllIso C).(o1,o2) by A4,A5;
    then <^o1,o2^> <> {} & <^o2,o1^> <> {} by Def5;
    then m in (the Arrows of AllCoretr C).(o1,o2) by A6,Def4;
    hence thesis by A4;
  end;
  then reconsider
  A = AllIso C as with_units non empty SubCatStr of AllCoretr C
  by A1,ALTCAT_2:24;
  now
    let o be object of A, o1 be object of AllCoretr C such that
A7: o = o1;
    reconsider oo = o as object of C by Def5;
    idm o = idm oo by ALTCAT_2:34
      .= idm o1 by A7,ALTCAT_2:34;
    hence idm o1 in <^o,o^>;
  end;
  hence thesis by ALTCAT_2:def 14;
end;

theorem Th43:
  AllCoretr C is non empty subcategory of AllMono C
proof
  the carrier of AllCoretr C = the carrier of C by Def4;
  then
A1: the carrier of AllCoretr C c= the carrier of AllMono C by Def1;
  the Arrows of AllCoretr C cc= the Arrows of AllMono C
  proof
    thus [:the carrier of AllCoretr C,the carrier of AllCoretr C:] c= [:the
    carrier of AllMono C,the carrier of AllMono C:] by A1,ZFMISC_1:96;
    let i be set;
    assume
A2: i in [:the carrier of AllCoretr C,the carrier of AllCoretr C:];
    then consider o1, o2 being set such that
A3: o1 in the carrier of AllCoretr C & o2 in the carrier of AllCoretr C and
A4: i = [o1,o2] by ZFMISC_1:84;
    reconsider o1, o2 as object of C by A3,Def4;
    let m be set;
    assume
A5: m in (the Arrows of AllCoretr C).i;
    the Arrows of AllCoretr C cc= the Arrows of C by Def4;
    then (the Arrows of AllCoretr C).[o1,o2] c= (the Arrows of C).(o1,o2) by A2
,A4,ALTCAT_2:def 2;
    then reconsider m1 = m as Morphism of o1, o2 by A4,A5;
    m in (the Arrows of AllCoretr C).(o1,o2) by A4,A5;
    then
A6: m1 is coretraction by Def4;
A7: m1 in (the Arrows of AllCoretr C).(o1,o2) by A4,A5;
    then
A8: <^o1,o2^> <> {} by Def4;
    <^o2,o1^> <> {} by A7,Def4;
    then m1 is mono by A8,A6,ALTCAT_3:16;
    then m in (the Arrows of AllMono C).(o1,o2) by A8,Def1;
    hence thesis by A4;
  end;
  then reconsider
  A = AllCoretr C as with_units non empty SubCatStr of AllMono C
  by A1,ALTCAT_2:24;
  now
    let o be object of A, o1 be object of AllMono C such that
A9: o = o1;
    reconsider oo = o as object of C by Def4;
    idm o = idm oo by ALTCAT_2:34
      .= idm o1 by A9,ALTCAT_2:34;
    hence idm o1 in <^o,o^>;
  end;
  hence thesis by ALTCAT_2:def 14;
end;

theorem Th44:
  AllRetr C is non empty subcategory of AllEpi C
proof
  the carrier of AllRetr C = the carrier of C by Def3;
  then
A1: the carrier of AllRetr C c= the carrier of AllEpi C by Def2;
  the Arrows of AllRetr C cc= the Arrows of AllEpi C
  proof
    thus [:the carrier of AllRetr C,the carrier of AllRetr C:] c= [:the
    carrier of AllEpi C,the carrier of AllEpi C:] by A1,ZFMISC_1:96;
    let i be set;
    assume
A2: i in [:the carrier of AllRetr C,the carrier of AllRetr C:];
    then consider o1, o2 being set such that
A3: o1 in the carrier of AllRetr C & o2 in the carrier of AllRetr C and
A4: i = [o1,o2] by ZFMISC_1:84;
    reconsider o1, o2 as object of C by A3,Def3;
    let m be set;
    assume
A5: m in (the Arrows of AllRetr C).i;
    the Arrows of AllRetr C cc= the Arrows of C by Def3;
    then (the Arrows of AllRetr C).[o1,o2] c= (the Arrows of C).(o1,o2) by A2
,A4,ALTCAT_2:def 2;
    then reconsider m1 = m as Morphism of o1, o2 by A4,A5;
    m in (the Arrows of AllRetr C).(o1,o2) by A4,A5;
    then
A6: m1 is retraction by Def3;
A7: m1 in (the Arrows of AllRetr C).(o1,o2) by A4,A5;
    then
A8: <^o1,o2^> <> {} by Def3;
    <^o2,o1^> <> {} by A7,Def3;
    then m1 is epi by A8,A6,ALTCAT_3:15;
    then m in (the Arrows of AllEpi C).(o1,o2) by A8,Def2;
    hence thesis by A4;
  end;
  then reconsider
  A = AllRetr C as with_units non empty SubCatStr of AllEpi C by A1,ALTCAT_2:24
;
  now
    let o be object of A, o1 be object of AllEpi C such that
A9: o = o1;
    reconsider oo = o as object of C by Def3;
    idm o = idm oo by ALTCAT_2:34
      .= idm o1 by A9,ALTCAT_2:34;
    hence idm o1 in <^o,o^>;
  end;
  hence thesis by ALTCAT_2:def 14;
end;

theorem
  (for o1, o2 being object of C, m being Morphism of o1, o2 holds m is
  mono ) implies the AltCatStr of C = AllMono C
proof
  assume
A1: for o1, o2 being object of C, m being Morphism of o1, o2 holds m is mono;
A2: the carrier of AllMono C = the carrier of the AltCatStr of C by Def1;
A3: the Arrows of AllMono C cc= the Arrows of C by Def1;
  now
    let i be set;
    assume
A4: i in [:the carrier of C,the carrier of C:];
    then consider o1, o2 being set such that
A5: o1 in the carrier of C & o2 in the carrier of C and
A6: i = [o1,o2] by ZFMISC_1:84;
    reconsider o1, o2 as object of C by A5;
    thus (the Arrows of AllMono C).i = (the Arrows of C).i
    proof
      thus (the Arrows of AllMono C).i c= (the Arrows of C).i by A2,A3,A4,
ALTCAT_2:def 2;
      let n be set;
      assume
A7:   n in (the Arrows of C).i;
      then reconsider n1 = n as Morphism of o1, o2 by A6;
      n1 is mono by A1;
      then n in (the Arrows of AllMono C).(o1,o2) by A6,A7,Def1;
      hence thesis by A6;
    end;
  end;
  hence thesis by A2,ALTCAT_2:25,PBOOLE:3;
end;

theorem
  (for o1, o2 being object of C, m being Morphism of o1, o2 holds m is
  epi ) implies the AltCatStr of C = AllEpi C
proof
  assume
A1: for o1, o2 being object of C, m being Morphism of o1, o2 holds m is epi;
A2: the carrier of AllEpi C = the carrier of the AltCatStr of C by Def2;
A3: the Arrows of AllEpi C cc= the Arrows of C by Def2;
  now
    let i be set;
    assume
A4: i in [:the carrier of C,the carrier of C:];
    then consider o1, o2 being set such that
A5: o1 in the carrier of C & o2 in the carrier of C and
A6: i = [o1,o2] by ZFMISC_1:84;
    reconsider o1, o2 as object of C by A5;
    thus (the Arrows of AllEpi C).i = (the Arrows of C).i
    proof
      thus (the Arrows of AllEpi C).i c= (the Arrows of C).i by A2,A3,A4,
ALTCAT_2:def 2;
      let n be set;
      assume
A7:   n in (the Arrows of C).i;
      then reconsider n1 = n as Morphism of o1, o2 by A6;
      n1 is epi by A1;
      then n in (the Arrows of AllEpi C).(o1,o2) by A6,A7,Def2;
      hence thesis by A6;
    end;
  end;
  hence thesis by A2,ALTCAT_2:25,PBOOLE:3;
end;

theorem
  (for o1, o2 being object of C, m being Morphism of o1, o2 holds m is
  retraction & <^o2,o1^> <> {}) implies the AltCatStr of C = AllRetr C
proof
  assume
A1: for o1, o2 being object of C, m being Morphism of o1, o2 holds m is
  retraction & <^o2,o1^> <> {};
A2: the carrier of AllRetr C = the carrier of the AltCatStr of C by Def3;
A3: the Arrows of AllRetr C cc= the Arrows of C by Def3;
  now
    let i be set;
    assume
A4: i in [:the carrier of C,the carrier of C:];
    then consider o1, o2 being set such that
A5: o1 in the carrier of C & o2 in the carrier of C and
A6: i = [o1,o2] by ZFMISC_1:84;
    reconsider o1, o2 as object of C by A5;
    thus (the Arrows of AllRetr C).i = (the Arrows of C).i
    proof
      thus (the Arrows of AllRetr C).i c= (the Arrows of C).i by A2,A3,A4,
ALTCAT_2:def 2;
      let n be set;
      assume
A7:   n in (the Arrows of C).i;
      then reconsider n1 = n as Morphism of o1, o2 by A6;
      <^o2,o1^> <> {} & n1 is retraction by A1;
      then n in (the Arrows of AllRetr C).(o1,o2) by A6,A7,Def3;
      hence thesis by A6;
    end;
  end;
  hence thesis by A2,ALTCAT_2:25,PBOOLE:3;
end;

theorem
  (for o1, o2 being object of C, m being Morphism of o1, o2 holds m is
  coretraction & <^o2,o1^> <> {}) implies the AltCatStr of C = AllCoretr C
proof
  assume
A1: for o1, o2 being object of C, m being Morphism of o1, o2 holds m is
  coretraction & <^o2,o1^> <> {};
A2: the carrier of AllCoretr C = the carrier of the AltCatStr of C by Def4;
A3: the Arrows of AllCoretr C cc= the Arrows of C by Def4;
  now
    let i be set;
    assume
A4: i in [:the carrier of C,the carrier of C:];
    then consider o1, o2 being set such that
A5: o1 in the carrier of C & o2 in the carrier of C and
A6: i = [o1,o2] by ZFMISC_1:84;
    reconsider o1, o2 as object of C by A5;
    thus (the Arrows of AllCoretr C).i = (the Arrows of C).i
    proof
      thus (the Arrows of AllCoretr C).i c= (the Arrows of C).i by A2,A3,A4,
ALTCAT_2:def 2;
      let n be set;
      assume
A7:   n in (the Arrows of C).i;
      then reconsider n1 = n as Morphism of o1, o2 by A6;
      <^o2,o1^> <> {} & n1 is coretraction by A1;
      then n in (the Arrows of AllCoretr C).(o1,o2) by A6,A7,Def4;
      hence thesis by A6;
    end;
  end;
  hence thesis by A2,ALTCAT_2:25,PBOOLE:3;
end;

theorem
  (for o1, o2 being object of C, m being Morphism of o1, o2 holds m is
  iso & <^o2,o1^> <> {}) implies the AltCatStr of C = AllIso C
proof
  assume
A1: for o1, o2 being object of C, m being Morphism of o1, o2 holds m is
  iso & <^o2,o1^> <> {};
A2: the carrier of AllIso C = the carrier of the AltCatStr of C by Def5;
A3: the Arrows of AllIso C cc= the Arrows of C by Def5;
  now
    let i be set;
    assume
A4: i in [:the carrier of C,the carrier of C:];
    then consider o1, o2 being set such that
A5: o1 in the carrier of C & o2 in the carrier of C and
A6: i = [o1,o2] by ZFMISC_1:84;
    reconsider o1, o2 as object of C by A5;
    thus (the Arrows of AllIso C).i = (the Arrows of C).i
    proof
      thus (the Arrows of AllIso C).i c= (the Arrows of C).i by A2,A3,A4,
ALTCAT_2:def 2;
      let n be set;
      assume
A7:   n in (the Arrows of C).i;
      then reconsider n1 = n as Morphism of o1, o2 by A6;
      <^o2,o1^> <> {} & n1 is iso by A1;
      then n in (the Arrows of AllIso C).(o1,o2) by A6,A7,Def5;
      hence thesis by A6;
    end;
  end;
  hence thesis by A2,ALTCAT_2:25,PBOOLE:3;
end;

theorem Th50:
  for o1, o2 being object of AllMono C for m being Morphism of o1,
  o2 st <^o1,o2^> <> {} holds m is mono
proof
  let o1, o2 be object of AllMono C, m be Morphism of o1, o2 such that
A1: <^o1,o2^> <> {};
  reconsider p1 = o1, p2 = o2 as object of C by Def1;
  reconsider p = m as Morphism of p1, p2 by A1,ALTCAT_2:33;
  p is mono by A1,Def1;
  hence thesis by A1,Th37;
end;

theorem Th51:
  for o1, o2 being object of AllEpi C for m being Morphism of o1,
  o2 st <^o1,o2^> <> {} holds m is epi
proof
  let o1, o2 be object of AllEpi C, m be Morphism of o1, o2 such that
A1: <^o1,o2^> <> {};
  reconsider p1 = o1, p2 = o2 as object of C by Def2;
  reconsider p = m as Morphism of p1, p2 by A1,ALTCAT_2:33;
  p is epi by A1,Def2;
  hence thesis by A1,Th37;
end;

theorem Th52:
  for o1, o2 being object of AllIso C for m being Morphism of o1,
  o2 st <^o1,o2^> <> {} holds m is iso & m" in <^o2,o1^>
proof
  let o1, o2 be object of AllIso C, m be Morphism of o1, o2 such that
A1: <^o1,o2^> <> {};
  reconsider p1 = o1, p2 = o2 as object of C by Def5;
  reconsider p = m as Morphism of p1, p2 by A1,ALTCAT_2:33;
  p in (the Arrows of AllIso C).(o1,o2) by A1;
  then
A2: <^p1,p2^> <> {} & <^p2,p1^> <> {} by Def5;
A3: p is iso by A1,Def5;
  then
A4: p" is iso by A2,Th3;
  then
A5: p" in (the Arrows of AllIso C).(p2,p1) by A2,Def5;
  reconsider m1 = p" as Morphism of o2, o1 by A2,A4,Def5;
A6: m is retraction
  proof
    take m1;
    thus m * m1 = p * p" by A1,A5,ALTCAT_2:32
      .= idm p2 by A3,ALTCAT_3:def 5
      .= idm o2 by ALTCAT_2:34;
  end;
A7: m is coretraction
  proof
    take m1;
    thus m1 * m = p" * p by A1,A5,ALTCAT_2:32
      .= idm p1 by A3,ALTCAT_3:def 5
      .= idm o1 by ALTCAT_2:34;
  end;
  p" in <^o2,o1^> by A2,A4,Def5;
  hence m is iso by A1,A6,A7,ALTCAT_3:6;
  thus thesis by A5;
end;

theorem
  AllMono AllMono C = AllMono C
proof
A1: the carrier of AllMono AllMono C = the carrier of AllMono C & the
  carrier of AllMono C = the carrier of C by Def1;
A2: the Arrows of AllMono AllMono C cc= the Arrows of AllMono C by Def1;
  now
    let i be set;
    assume
A3: i in [:the carrier of C,the carrier of C:];
    then consider o1, o2 being set such that
A4: o1 in the carrier of C & o2 in the carrier of C and
A5: i = [o1,o2] by ZFMISC_1:84;
    reconsider o1, o2 as object of AllMono C by A4,Def1;
    thus (the Arrows of AllMono AllMono C).i = (the Arrows of AllMono C).i
    proof
      thus (the Arrows of AllMono AllMono C).i c= (the Arrows of AllMono C).i
      by A1,A2,A3,ALTCAT_2:def 2;
      let n be set;
      assume
A6:   n in (the Arrows of AllMono C).i;
      then reconsider n1 = n as Morphism of o1, o2 by A5;
      n1 is mono by A5,A6,Th50;
      then n in (the Arrows of AllMono AllMono C).(o1,o2) by A5,A6,Def1;
      hence thesis by A5;
    end;
  end;
  hence thesis by A1,ALTCAT_2:25,PBOOLE:3;
end;

theorem
  AllEpi AllEpi C = AllEpi C
proof
A1: the carrier of AllEpi AllEpi C = the carrier of AllEpi C & the carrier
  of AllEpi C = the carrier of C by Def2;
A2: the Arrows of AllEpi AllEpi C cc= the Arrows of AllEpi C by Def2;
  now
    let i be set;
    assume
A3: i in [:the carrier of C,the carrier of C:];
    then consider o1, o2 being set such that
A4: o1 in the carrier of C & o2 in the carrier of C and
A5: i = [o1,o2] by ZFMISC_1:84;
    reconsider o1, o2 as object of AllEpi C by A4,Def2;
    thus (the Arrows of AllEpi AllEpi C).i = (the Arrows of AllEpi C).i
    proof
      thus (the Arrows of AllEpi AllEpi C).i c= (the Arrows of AllEpi C).i by
A1,A2,A3,ALTCAT_2:def 2;
      let n be set;
      assume
A6:   n in (the Arrows of AllEpi C).i;
      then reconsider n1 = n as Morphism of o1, o2 by A5;
      n1 is epi by A5,A6,Th51;
      then n in (the Arrows of AllEpi AllEpi C).(o1,o2) by A5,A6,Def2;
      hence thesis by A5;
    end;
  end;
  hence thesis by A1,ALTCAT_2:25,PBOOLE:3;
end;

theorem
  AllIso AllIso C = AllIso C
proof
A1: the carrier of AllIso AllIso C = the carrier of AllIso C & the carrier
  of AllIso C = the carrier of C by Def5;
A2: the Arrows of AllIso AllIso C cc= the Arrows of AllIso C by Def5;
  now
    let i be set;
    assume
A3: i in [:the carrier of C,the carrier of C:];
    then consider o1, o2 being set such that
A4: o1 in the carrier of C & o2 in the carrier of C and
A5: i = [o1,o2] by ZFMISC_1:84;
    reconsider o1, o2 as object of AllIso C by A4,Def5;
    thus (the Arrows of AllIso AllIso C).i = (the Arrows of AllIso C).i
    proof
      thus (the Arrows of AllIso AllIso C).i c= (the Arrows of AllIso C).i by
A1,A2,A3,ALTCAT_2:def 2;
      let n be set;
      assume
A6:   n in (the Arrows of AllIso C).i;
      then reconsider n1 = n as Morphism of o1, o2 by A5;
      n1" in <^o2,o1^> & n1 is iso by A5,A6,Th52;
      then n in (the Arrows of AllIso AllIso C).(o1,o2) by A5,A6,Def5;
      hence thesis by A5;
    end;
  end;
  hence thesis by A1,ALTCAT_2:25,PBOOLE:3;
end;

theorem
  AllIso AllMono C = AllIso C
proof
A1: AllIso AllMono C is transitive non empty SubCatStr of C by ALTCAT_2:21;
A2: the carrier of AllIso AllMono C = the carrier of AllMono C by Def5;
A3: the carrier of AllIso C = the carrier of C by Def5;
A4: the carrier of AllMono C = the carrier of C by Def1;
  AllIso C is non empty subcategory of AllCoretr C & AllCoretr C is non
  empty subcategory of AllMono C by Th42,Th43;
  then
A5: AllIso C is non empty subcategory of AllMono C by Th36;
A6: now
    let i be set;
    assume
A7: i in [:the carrier of C,the carrier of C:];
    then consider o1, o2 being set such that
A8: o1 in the carrier of C & o2 in the carrier of C and
A9: i = [o1,o2] by ZFMISC_1:84;
    reconsider o1, o2 as object of AllMono C by A8,Def1;
    thus (the Arrows of AllIso AllMono C).i = (the Arrows of AllIso C).i
    proof
      thus (the Arrows of AllIso AllMono C).i c= (the Arrows of AllIso C).i
      proof
        reconsider r1 = o1, r2 = o2 as object of C by Def1;
        reconsider q1 = o1, q2 = o2 as object of AllIso AllMono C by Def5;
A10:    <^q2,q1^> c= <^o2,o1^> by ALTCAT_2:31;
        let n be set such that
A11:    n in (the Arrows of AllIso AllMono C).i;
        n in <^q1,q2^> by A9,A11;
        then
A12:    <^o2,o1^> <> {} by A10,Th52;
        then
A13:    <^r2,r1^> <> {} by ALTCAT_2:31,XBOOLE_1:3;
A14:    <^q1,q2^> c= <^o1,o2^> by ALTCAT_2:31;
        then reconsider n2 = n as Morphism of o1, o2 by A9,A11;
A15:    <^r1,r2^> <> {} by A9,A11,A14,ALTCAT_2:31,XBOOLE_1:3;
        <^o1,o2^> c= <^r1,r2^> by ALTCAT_2:31;
        then <^q1,q2^> c= <^r1,r2^> by A14,XBOOLE_1:1;
        then reconsider n1 = n as Morphism of r1, r2 by A9,A11;
        n in (the Arrows of AllIso AllMono C).(q1,q2) by A9,A11;
        then n2 is iso by Def5;
        then n1 is iso by A9,A11,A14,A12,Th40;
        then n in (the Arrows of AllIso C).(r1,r2) by A15,A13,Def5;
        hence thesis by A9;
      end;
      reconsider p1 = o1, p2 = o2 as object of AllIso C by A4,Def5;
A16:  <^p2,p1^> c= <^o2,o1^> by A5,ALTCAT_2:31;
      let n be set such that
A17:  n in (the Arrows of AllIso C).i;
      reconsider n2 = n as Morphism of p1, p2 by A9,A17;
      the Arrows of AllIso C cc= the Arrows of AllMono C by A5,ALTCAT_2:def 11;
      then
A18:  (the Arrows of AllIso C).i c= (the Arrows of AllMono C).i by A3,A7,
ALTCAT_2:def 2;
      then reconsider n1 = n as Morphism of o1, o2 by A9,A17;
A19:  n2" in <^p2,p1^> by A9,A17,Th52;
      n2 is iso by A9,A17,Th52;
      then n1 is iso by A5,A9,A17,A19,Th40;
      then
      n in (the Arrows of AllIso AllMono C).(o1,o2) by A9,A17,A18,A19,A16,Def5;
      hence thesis by A9;
    end;
  end;
  then the Arrows of AllIso AllMono C = the Arrows of AllIso C by A2,A3,A4,
PBOOLE:3;
  then AllIso AllMono C is SubCatStr of AllIso C by A2,A3,A4,A1,ALTCAT_2:24;
  hence thesis by A2,A3,A4,A6,ALTCAT_2:25,PBOOLE:3;
end;

theorem
  AllIso AllEpi C = AllIso C
proof
A1: AllIso AllEpi C is transitive non empty SubCatStr of C by ALTCAT_2:21;
A2: the carrier of AllIso AllEpi C = the carrier of AllEpi C by Def5;
A3: the carrier of AllIso C = the carrier of C by Def5;
A4: the carrier of AllEpi C = the carrier of C by Def2;
  AllIso C is non empty subcategory of AllRetr C & AllRetr C is non empty
  subcategory of AllEpi C by Th41,Th44;
  then
A5: AllIso C is non empty subcategory of AllEpi C by Th36;
A6: now
    let i be set;
    assume
A7: i in [:the carrier of C,the carrier of C:];
    then consider o1, o2 being set such that
A8: o1 in the carrier of C & o2 in the carrier of C and
A9: i = [o1,o2] by ZFMISC_1:84;
    reconsider o1, o2 as object of AllEpi C by A8,Def2;
    thus (the Arrows of AllIso AllEpi C).i = (the Arrows of AllIso C).i
    proof
      thus (the Arrows of AllIso AllEpi C).i c= (the Arrows of AllIso C).i
      proof
        reconsider r1 = o1, r2 = o2 as object of C by Def2;
        reconsider q1 = o1, q2 = o2 as object of AllIso AllEpi C by Def5;
A10:    <^q2,q1^> c= <^o2,o1^> by ALTCAT_2:31;
        let n be set such that
A11:    n in (the Arrows of AllIso AllEpi C).i;
        n in <^q1,q2^> by A9,A11;
        then
A12:    <^o2,o1^> <> {} by A10,Th52;
        then
A13:    <^r2,r1^> <> {} by ALTCAT_2:31,XBOOLE_1:3;
A14:    <^q1,q2^> c= <^o1,o2^> by ALTCAT_2:31;
        then reconsider n2 = n as Morphism of o1, o2 by A9,A11;
A15:    <^r1,r2^> <> {} by A9,A11,A14,ALTCAT_2:31,XBOOLE_1:3;
        <^o1,o2^> c= <^r1,r2^> by ALTCAT_2:31;
        then <^q1,q2^> c= <^r1,r2^> by A14,XBOOLE_1:1;
        then reconsider n1 = n as Morphism of r1, r2 by A9,A11;
        n in (the Arrows of AllIso AllEpi C).(q1,q2) by A9,A11;
        then n2 is iso by Def5;
        then n1 is iso by A9,A11,A14,A12,Th40;
        then n in (the Arrows of AllIso C).(r1,r2) by A15,A13,Def5;
        hence thesis by A9;
      end;
      reconsider p1 = o1, p2 = o2 as object of AllIso C by A4,Def5;
A16:  <^p2,p1^> c= <^o2,o1^> by A5,ALTCAT_2:31;
      let n be set such that
A17:  n in (the Arrows of AllIso C).i;
      reconsider n2 = n as Morphism of p1, p2 by A9,A17;
      the Arrows of AllIso C cc= the Arrows of AllEpi C by A5,ALTCAT_2:def 11;
      then
A18:  (the Arrows of AllIso C).i c= (the Arrows of AllEpi C).i by A3,A7,
ALTCAT_2:def 2;
      then reconsider n1 = n as Morphism of o1, o2 by A9,A17;
A19:  n2" in <^p2,p1^> by A9,A17,Th52;
      n2 is iso by A9,A17,Th52;
      then n1 is iso by A5,A9,A17,A19,Th40;
      then n in (the Arrows of AllIso AllEpi C).(o1,o2) by A9,A17,A18,A19,A16
,Def5;
      hence thesis by A9;
    end;
  end;
  then the Arrows of AllIso AllEpi C = the Arrows of AllIso C by A2,A3,A4,
PBOOLE:3;
  then AllIso AllEpi C is SubCatStr of AllIso C by A2,A3,A4,A1,ALTCAT_2:24;
  hence thesis by A2,A3,A4,A6,ALTCAT_2:25,PBOOLE:3;
end;

theorem
  AllIso AllRetr C = AllIso C
proof
A1: AllIso AllRetr C is transitive non empty SubCatStr of C by ALTCAT_2:21;
A2: the carrier of AllIso AllRetr C = the carrier of AllRetr C by Def5;
A3: the carrier of AllIso C = the carrier of C by Def5;
A4: the carrier of AllRetr C = the carrier of C by Def3;
A5: AllIso C is non empty subcategory of AllRetr C by Th41;
A6: now
    let i be set;
    assume
A7: i in [:the carrier of C,the carrier of C:];
    then consider o1, o2 being set such that
A8: o1 in the carrier of C & o2 in the carrier of C and
A9: i = [o1,o2] by ZFMISC_1:84;
    reconsider o1, o2 as object of AllRetr C by A8,Def3;
    thus (the Arrows of AllIso AllRetr C).i = (the Arrows of AllIso C).i
    proof
      thus (the Arrows of AllIso AllRetr C).i c= (the Arrows of AllIso C).i
      proof
        reconsider r1 = o1, r2 = o2 as object of C by Def3;
        reconsider q1 = o1, q2 = o2 as object of AllIso AllRetr C by Def5;
A10:    <^q2,q1^> c= <^o2,o1^> by ALTCAT_2:31;
        let n be set such that
A11:    n in (the Arrows of AllIso AllRetr C).i;
        n in <^q1,q2^> by A9,A11;
        then
A12:    <^o2,o1^> <> {} by A10,Th52;
        then
A13:    <^r2,r1^> <> {} by ALTCAT_2:31,XBOOLE_1:3;
A14:    <^q1,q2^> c= <^o1,o2^> by ALTCAT_2:31;
        then reconsider n2 = n as Morphism of o1, o2 by A9,A11;
A15:    <^r1,r2^> <> {} by A9,A11,A14,ALTCAT_2:31,XBOOLE_1:3;
        <^o1,o2^> c= <^r1,r2^> by ALTCAT_2:31;
        then <^q1,q2^> c= <^r1,r2^> by A14,XBOOLE_1:1;
        then reconsider n1 = n as Morphism of r1, r2 by A9,A11;
        n in (the Arrows of AllIso AllRetr C).(q1,q2) by A9,A11;
        then n2 is iso by Def5;
        then n1 is iso by A9,A11,A14,A12,Th40;
        then n in (the Arrows of AllIso C).(r1,r2) by A15,A13,Def5;
        hence thesis by A9;
      end;
      reconsider p1 = o1, p2 = o2 as object of AllIso C by A4,Def5;
A16:  <^p2,p1^> c= <^o2,o1^> by A5,ALTCAT_2:31;
      let n be set such that
A17:  n in (the Arrows of AllIso C).i;
      reconsider n2 = n as Morphism of p1, p2 by A9,A17;
      the Arrows of AllIso C cc= the Arrows of AllRetr C by A5,ALTCAT_2:def 11;
      then
A18:  (the Arrows of AllIso C).i c= (the Arrows of AllRetr C).i by A3,A7,
ALTCAT_2:def 2;
      then reconsider n1 = n as Morphism of o1, o2 by A9,A17;
A19:  n2" in <^p2,p1^> by A9,A17,Th52;
      n2 is iso by A9,A17,Th52;
      then n1 is iso by A5,A9,A17,A19,Th40;
      then
      n in (the Arrows of AllIso AllRetr C).(o1,o2) by A9,A17,A18,A19,A16,Def5;
      hence thesis by A9;
    end;
  end;
  then the Arrows of AllIso AllRetr C = the Arrows of AllIso C by A2,A3,A4,
PBOOLE:3;
  then AllIso AllRetr C is SubCatStr of AllIso C by A2,A3,A4,A1,ALTCAT_2:24;
  hence thesis by A2,A3,A4,A6,ALTCAT_2:25,PBOOLE:3;
end;

theorem
  AllIso AllCoretr C = AllIso C
proof
A1: AllIso AllCoretr C is transitive non empty SubCatStr of C by ALTCAT_2:21;
A2: the carrier of AllIso AllCoretr C = the carrier of AllCoretr C by Def5;
A3: the carrier of AllIso C = the carrier of C by Def5;
A4: the carrier of AllCoretr C = the carrier of C by Def4;
A5: AllIso C is non empty subcategory of AllCoretr C by Th42;
A6: now
    let i be set;
    assume
A7: i in [:the carrier of C,the carrier of C:];
    then consider o1, o2 being set such that
A8: o1 in the carrier of C & o2 in the carrier of C and
A9: i = [o1,o2] by ZFMISC_1:84;
    reconsider o1, o2 as object of AllCoretr C by A8,Def4;
    thus (the Arrows of AllIso AllCoretr C).i = (the Arrows of AllIso C).i
    proof
      thus (the Arrows of AllIso AllCoretr C).i c= (the Arrows of AllIso C).i
      proof
        reconsider r1 = o1, r2 = o2 as object of C by Def4;
        reconsider q1 = o1, q2 = o2 as object of AllIso AllCoretr C by Def5;
A10:    <^q2,q1^> c= <^o2,o1^> by ALTCAT_2:31;
        let n be set such that
A11:    n in (the Arrows of AllIso AllCoretr C).i;
        n in <^q1,q2^> by A9,A11;
        then
A12:    <^o2,o1^> <> {} by A10,Th52;
        then
A13:    <^r2,r1^> <> {} by ALTCAT_2:31,XBOOLE_1:3;
A14:    <^q1,q2^> c= <^o1,o2^> by ALTCAT_2:31;
        then reconsider n2 = n as Morphism of o1, o2 by A9,A11;
A15:    <^r1,r2^> <> {} by A9,A11,A14,ALTCAT_2:31,XBOOLE_1:3;
        <^o1,o2^> c= <^r1,r2^> by ALTCAT_2:31;
        then <^q1,q2^> c= <^r1,r2^> by A14,XBOOLE_1:1;
        then reconsider n1 = n as Morphism of r1, r2 by A9,A11;
        n in (the Arrows of AllIso AllCoretr C).(q1,q2) by A9,A11;
        then n2 is iso by Def5;
        then n1 is iso by A9,A11,A14,A12,Th40;
        then n in (the Arrows of AllIso C).(r1,r2) by A15,A13,Def5;
        hence thesis by A9;
      end;
      reconsider p1 = o1, p2 = o2 as object of AllIso C by A4,Def5;
A16:  <^p2,p1^> c= <^o2,o1^> by A5,ALTCAT_2:31;
      let n be set such that
A17:  n in (the Arrows of AllIso C).i;
      reconsider n2 = n as Morphism of p1, p2 by A9,A17;
      the Arrows of AllIso C cc= the Arrows of AllCoretr C by A5,
ALTCAT_2:def 11;
      then
A18:  (the Arrows of AllIso C).i c= (the Arrows of AllCoretr C).i by A3,A7,
ALTCAT_2:def 2;
      then reconsider n1 = n as Morphism of o1, o2 by A9,A17;
A19:  n2" in <^p2,p1^> by A9,A17,Th52;
      n2 is iso by A9,A17,Th52;
      then n1 is iso by A5,A9,A17,A19,Th40;
      then
      n in (the Arrows of AllIso AllCoretr C).(o1,o2) by A9,A17,A18,A19,A16
,Def5;
      hence thesis by A9;
    end;
  end;
  then the Arrows of AllIso AllCoretr C = the Arrows of AllIso C by A2,A3,A4,
PBOOLE:3;
  then AllIso AllCoretr C is SubCatStr of AllIso C by A2,A3,A4,A1,ALTCAT_2:24;
  hence thesis by A2,A3,A4,A6,ALTCAT_2:25,PBOOLE:3;
end;