defpred S₁[ object , object ] means ex D2 being set st
( D2 = $2 & ( for x being set holds
( x in D2 iff ex o1, o2 being Object of C ex 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 object st i in [: the carrier of C, the carrier of C:] holds
ex X being object st S₁[i,X]

let i be object ; :: thesis:
assume i in [: the carrier of C, the carrier of C:] ; :: thesis:
then consider o1, o2 being object such that
A2: ( o1 in the carrier of C & o2 in the carrier of C ) and
A3: i = [o1,o2] by ZFMISC_1:84;
reconsider o1 = o1, o2 = o2 as Object of C by A2;
defpred S₂[ object ] 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 object holds
( x in X iff ( x in the Arrows of C . (o1,o2) & S₂[x] ) ) from XBOOLE_0:sch 1();
take X ; :: thesis:
take X ; :: thesis:
thus X = X ; :: thesis:
let x be set ; :: thesis:
thus ( x in X implies ex o1, o2 being Object of C ex m being Morphism of o1,o2 st
( i = [o1,o2] & <^o1,o2^> <> {} & x = m & m is mono ) ) :: thesis:

assume x in X ; :: thesis:
then consider m being Morphism of o1,o2 such that
A5: ( <^o1,o2^> <> {} & m = x & m is mono ) by A4;
take o1 ; :: thesis:
take o2 ; :: thesis:
take m ; :: thesis:
thus ( i = [o1,o2] & <^o1,o2^> <> {} & x = m & m is mono ) by A3, A5; :: thesis:

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 ) ; :: thesis:
( o1 = p1 & o2 = p2 ) by A3, A6, XTUPLE_0:1;
hence x in X by A4, A7; :: thesis:

end;

consider Ar being ManySortedSet of [: the carrier of C, the carrier of C:] such that
A8: for i being object st i in [: the carrier of C, the carrier of C:] holds
S₁[i,Ar . i] from PBOOLE:sch 3(A1);
defpred S₂[ object , object ] 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)):] );
A9: for i being object st i in [: the carrier of C, the carrier of C, the carrier of C:] holds
ex j being object st S₂[i,j]

proof

let i be object ; :: thesis:
assume i in [: the carrier of C, the carrier of C, the carrier of C:] ; :: thesis:
then consider p1, p2, p3 being object such that
A10: ( p1 in the carrier of C & p2 in the carrier of C & p3 in the carrier of C ) and
A11: i = [p1,p2,p3] by MCART_1:68;
reconsider p1 = p1, p2 = p2, p3 = p3 as Object of C by A10;
take ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] ; :: thesis:
take p1 ; :: thesis:
take p2 ; :: thesis:
take p3 ; :: thesis:
thus i = [p1,p2,p3] by A11; :: thesis:
thus ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] = ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] ; :: thesis:

end;

consider Co being ManySortedSet of [: the carrier of C, the carrier of C, the carrier of C:] such that
A12: for i being object st i in [: the carrier of C, the carrier of C, the carrier of C:] holds
S₂[i,Co . i] from PBOOLE:sch 3(A9);
A13: Ar cc= the Arrows of C

proof

thus [: the carrier of C, the carrier of C:] c= [: the carrier of C, the carrier of C:] ; :: according to ALTCAT_2:def 2 :: thesis:
let i be set ; :: thesis:
assume A14: i in [: the carrier of C, the carrier of C:] ; :: thesis:
let q be object ; :: according to TARSKI:def 3 :: thesis:
assume A15: q in Ar . i ; :: thesis:
S₁[i,Ar . i] by A8, A14;
then ex p1, p2 being Object of C ex m being Morphism of p1,p2 st
( i = [p1,p2] & <^p1,p2^> <> {} & q = m & m is mono ) by A15;
hence q in the Arrows of C . i ; :: thesis:

end;

Co is ManySortedFunction of {|Ar,Ar|},{|Ar|}

proof

let i be object ; :: according to PBOOLE:def 15 :: thesis:
assume i in [: the carrier of C, the carrier of C, the carrier of C:] ; :: thesis:
then consider p1, p2, p3 being Object of C such that
A16: i = [p1,p2,p3] and
A17: Co . i = ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] by A12;
A18: [p1,p2] in [: the carrier of C, the carrier of C:] by ZFMISC_1:def 2;
then A19: Ar . [p1,p2] c= the Arrows of C . (p1,p2) by A13;
A20: [p2,p3] in [: the carrier of C, the carrier of C:] by ZFMISC_1:def 2;
then Ar . [p2,p3] c= the Arrows of C . (p2,p3) by A13;
then A21: [:(Ar . (p2,p3)),(Ar . (p1,p2)):] c= [:( the Arrows of C . (p2,p3)),( the Arrows of C . (p1,p2)):] by A19, 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 A17, A21, FUNCT_2:32;
A22: Ar . [p1,p2] c= the Arrows of C . [p1,p2] by A13, A18;
A23: Ar . [p2,p3] c= the Arrows of C . [p2,p3] by A13, A20;
A24: ( the Arrows of C . (p1,p3) = {} implies [:(Ar . (p2,p3)),(Ar . (p1,p2)):] = {} )

proof

assume A25: the Arrows of C . (p1,p3) = {} ; :: thesis:
assume [:(Ar . (p2,p3)),(Ar . (p1,p2)):] <> {} ; :: thesis:
then consider k being object such that
A26: k in [:(Ar . (p2,p3)),(Ar . (p1,p2)):] by XBOOLE_0:def 1;
consider u1, u2 being object such that
A27: ( u1 in Ar . (p2,p3) & u2 in Ar . (p1,p2) ) and
k = [u1,u2] by A26, ZFMISC_1:def 2;
( u1 in <^p2,p3^> & u2 in <^p1,p2^> ) by A23, A22, A27;
then <^p1,p3^> <> {} by ALTCAT_1:def 2;
hence contradiction by A25; :: thesis:

end;

A28: {|Ar|} . (p1,p2,p3) = Ar . (p1,p3) by ALTCAT_1:def 3;
A29: rng f c= {|Ar|} . i

proof

let q be object ; :: according to TARSKI:def 3 :: thesis:
assume q in rng f ; :: thesis:
then consider x being object such that
A30: x in dom f and
A31: q = f . x by FUNCT_1:def 3;
A32: dom f = [:(Ar . (p2,p3)),(Ar . (p1,p2)):] by A24, FUNCT_2:def 1;
then consider m1, m2 being object such that
A33: m1 in Ar . (p2,p3) and
A34: m2 in Ar . (p1,p2) and
A35: x = [m1,m2] by A30, ZFMISC_1:84;
[p2,p3] in [: the carrier of C, the carrier of C:] by ZFMISC_1:def 2;
then S₁[[p2,p3],Ar . [p2,p3]] by A8;
then consider q2, q3 being Object of C, qq being Morphism of q2,q3 such that
A36: [p2,p3] = [q2,q3] and
A37: <^q2,q3^> <> {} and
A38: m1 = qq and
A39: qq is mono by A33;
[p1,p2] in [: the carrier of C, the carrier of C:] by ZFMISC_1:def 2;
then S₁[[p1,p2],Ar . [p1,p2]] by A8;
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: m2 = rr and
A43: rr is mono by A34;
A44: ex o1, o3 being Object of C ex m being Morphism of o1,o3 st
( [p1,p3] = [o1,o3] & <^o1,o3^> <> {} & q = m & m is mono )

proof

A45: p2 = q2 by A36, XTUPLE_0:1;
then reconsider mm = qq as Morphism of r2,q3 by A40, XTUPLE_0:1;
take r1 ; :: thesis:
take q3 ; :: thesis:
take mm * rr ; :: thesis:
A46: p1 = r1 by A40, XTUPLE_0:1;
hence [p1,p3] = [r1,q3] by A36, XTUPLE_0:1; :: thesis:
A47: r2 = p2 by A40, XTUPLE_0:1;
hence <^r1,q3^> <> {} by A37, A41, A45, ALTCAT_1:def 2; :: thesis:
A48: p3 = q3 by A36, XTUPLE_0:1;
thus q = ( the Comp of C . (p1,p2,p3)) . (mm,rr) by A17, A30, A31, A32, A35, A38, A42, FUNCT_1:49
.= mm * rr by A36, A37, A41, A47, A46, A48, ALTCAT_1:def 8 ; :: thesis:
thus mm * rr is mono by A37, A39, A41, A43, A47, A45, ALTCAT_3:9; :: thesis:

end;

[p1,p3] in [: the carrier of C, the carrier of C:] by ZFMISC_1:def 2;
then S₁[[p1,p3],Ar . [p1,p3]] by A8;
then q in Ar . [p1,p3] by A44;
hence q in {|Ar|} . i by A16, A28, MULTOP_1:def 1; :: thesis:

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 A16, MULTOP_1:def 1;
hence Co . i is M3( bool [:({|Ar,Ar|} . i),({|Ar|} . i):]) by A24, A29, FUNCT_2:6; :: thesis:

end;

then reconsider Co = Co as BinComp of Ar ;
set IT = AltCatStr(# the carrier of C,Ar,Co #);
set J = the carrier of AltCatStr(# the carrier of C,Ar,Co #);
AltCatStr(# the carrier of C,Ar,Co #) is SubCatStr of C

proof

thus the carrier of AltCatStr(# the carrier of C,Ar,Co #) c= the carrier of C ; :: according to ALTCAT_2:def 11 :: thesis:
thus the Arrows of AltCatStr(# the carrier of C,Ar,Co #) cc= the Arrows of C by A13; :: thesis:
thus [: the carrier of AltCatStr(# the carrier of C,Ar,Co #), the carrier of AltCatStr(# the carrier of C,Ar,Co #), the carrier of AltCatStr(# the carrier of C,Ar,Co #):] c= [: the carrier of C, the carrier of C, the carrier of C:] ; :: according to ALTCAT_2:def 2 :: thesis:
let i be set ; :: thesis:
assume i in [: the carrier of AltCatStr(# the carrier of C,Ar,Co #), the carrier of AltCatStr(# the carrier of C,Ar,Co #), the carrier of AltCatStr(# the carrier of C,Ar,Co #):] ; :: thesis:
then consider p1, p2, p3 being Object of C such that
A49: i = [p1,p2,p3] and
A50: Co . i = ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] by A12;
A51: ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] c= the Comp of C . (p1,p2,p3) by RELAT_1:59;
let q be object ; :: according to TARSKI:def 3 :: thesis:
assume q in the Comp of AltCatStr(# the carrier of C,Ar,Co #) . i ; :: thesis:
then q in the Comp of C . (p1,p2,p3) by A50, A51;
hence q in the Comp of C . i by A49, MULTOP_1:def 1; :: thesis:

end;

then reconsider IT = AltCatStr(# the carrier of C,Ar,Co #) as non empty strict SubCatStr of C ;
IT is transitive

proof

let p1, p2, p3 be Object of IT; :: according to ALTCAT_1:def 2 :: thesis:
assume that
A52: <^p1,p2^> <> {} and
A53: <^p2,p3^> <> {} ; :: thesis:
consider m2 being object such that
A54: m2 in <^p1,p2^> by A52, XBOOLE_0:def 1;
consider m1 being object such that
A55: m1 in <^p2,p3^> by A53, XBOOLE_0:def 1;
[p2,p3] in [: the carrier of C, the carrier of C:] by ZFMISC_1:def 2;
then S₁[[p2,p3],Ar . [p2,p3]] by A8;
then consider q2, q3 being Object of C, qq being Morphism of q2,q3 such that
A56: [p2,p3] = [q2,q3] and
A57: <^q2,q3^> <> {} and
m1 = qq and
A58: qq is mono by A55;
[p1,p2] in [: the carrier of C, the carrier of C:] by ZFMISC_1:def 2;
then S₁[[p1,p2],Ar . [p1,p2]] by A8;
then consider r1, r2 being Object of C, rr being Morphism of r1,r2 such that
A59: [p1,p2] = [r1,r2] and
A60: <^r1,r2^> <> {} and
m2 = rr and
A61: rr is mono by A54;
A62: p2 = q2 by A56, XTUPLE_0:1;
then reconsider mm = qq as Morphism of r2,q3 by A59, XTUPLE_0:1;
A63: r2 = p2 by A59, XTUPLE_0:1;
A64: ex o1, o3 being Object of C ex m being Morphism of o1,o3 st
( [p1,p3] = [o1,o3] & <^o1,o3^> <> {} & mm * rr = m & m is mono )

proof

take r1 ; :: thesis:
take q3 ; :: thesis:
take mm * rr ; :: thesis:
p1 = r1 by A59, XTUPLE_0:1;
hence [p1,p3] = [r1,q3] by A56, XTUPLE_0:1; :: thesis:
thus <^r1,q3^> <> {} by A57, A60, A63, A62, ALTCAT_1:def 2; :: thesis:
thus mm * rr = mm * rr ; :: thesis:
thus mm * rr is mono by A57, A58, A60, A61, A63, A62, ALTCAT_3:9; :: thesis:

end;

[p1,p3] in [: the carrier of C, the carrier of C:] by ZFMISC_1:def 2;
then S₁[[p1,p3],Ar . [p1,p3]] by A8;
hence not <^p1,p3^> = {} by A64; :: thesis:

end;

then reconsider IT = IT as non empty transitive strict SubCatStr of C ;
take IT ; :: thesis:
thus the carrier of IT = the carrier of C ; :: thesis:
thus the Arrows of IT cc= the Arrows of C by A13; :: thesis:
let o1, o2 be Object of C; :: thesis:
let m be Morphism of o1,o2; :: thesis:
A65: [o1,o2] in [: the carrier of C, the carrier of C:] by ZFMISC_1:def 2;
thus ( m in the Arrows of IT . (o1,o2) implies ( <^o1,o2^> <> {} & m is mono ) ) :: thesis:

proof

assume A66: m in the Arrows of IT . (o1,o2) ; :: thesis:
S₁[[o1,o2],Ar . [o1,o2]] by A8, A65;
then consider p1, p2 being Object of C, n being Morphism of p1,p2 such that
A67: [o1,o2] = [p1,p2] and
A68: ( <^p1,p2^> <> {} & m = n & n is mono ) by A66;
( o1 = p1 & o2 = p2 ) by A67, XTUPLE_0:1;
hence ( <^o1,o2^> <> {} & m is mono ) by A68; :: thesis:

end;

assume A69: ( <^o1,o2^> <> {} & m is mono ) ; :: thesis:
S₁[[o1,o2],Ar . [o1,o2]] by A8, A65;
hence m in the Arrows of IT . (o1,o2) by A69; :: thesis: