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^> <> {} & <^o2,o1^> <> {} & x = m & m is coretraction ) ) ) );
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^> <> {} & <^o2,o1^> <> {} & m = $1 & m is coretraction );
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^> <> {} & <^o2,o1^> <> {} & x = m & m is coretraction ) ) :: thesis:

assume x in X ; :: thesis:
then consider m being Morphism of o1,o2 such that
A5: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m = x & m is coretraction ) by A4;
take o1 ; :: thesis:
take o2 ; :: thesis:
take m ; :: thesis:
thus ( i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is coretraction ) 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^> <> {} & <^p2,p1^> <> {} & x = m & m is coretraction ) ; :: 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^> <> {} & <^p2,p1^> <> {} & q = m & m is coretraction ) 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: <^q3,q2^> <> {} and
A39: m1 = qq and
A40: qq is coretraction 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
A41: [p1,p2] = [r1,r2] and
A42: <^r1,r2^> <> {} and
A43: <^r2,r1^> <> {} and
A44: m2 = rr and
A45: rr is coretraction by A34;
A46: ex o1, o3 being Object of C ex m being Morphism of o1,o3 st
( [p1,p3] = [o1,o3] & <^o1,o3^> <> {} & <^o3,o1^> <> {} & q = m & m is coretraction )

proof

A47: p2 = q2 by A36, XTUPLE_0:1;
then reconsider mm = qq as Morphism of r2,q3 by A41, XTUPLE_0:1;
take r1 ; :: thesis:
take q3 ; :: thesis:
take mm * rr ; :: thesis:
A48: p1 = r1 by A41, XTUPLE_0:1;
hence [p1,p3] = [r1,q3] by A36, XTUPLE_0:1; :: thesis:
A49: r2 = p2 by A41, XTUPLE_0:1;
hence A50: ( <^r1,q3^> <> {} & <^q3,r1^> <> {} ) by A37, A38, A42, A43, A47, ALTCAT_1:def 2; :: thesis:
A51: p3 = q3 by A36, XTUPLE_0:1;
thus q = ( the Comp of C . (p1,p2,p3)) . (mm,rr) by A17, A30, A31, A32, A35, A39, A44, FUNCT_1:49
.= mm * rr by A36, A37, A42, A49, A48, A51, ALTCAT_1:def 8 ; :: thesis:
thus mm * rr is coretraction by A37, A40, A42, A45, A49, A47, A50, ALTCAT_3:19; :: 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 A46;
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
A52: i = [p1,p2,p3] and
A53: Co . i = ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] by A12;
A54: ( 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 A53, A54;
hence q in the Comp of C . i by A52, 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
A55: <^p1,p2^> <> {} and
A56: <^p2,p3^> <> {} ; :: thesis:
consider m2 being object such that
A57: m2 in <^p1,p2^> by A55, XBOOLE_0:def 1;
consider m1 being object such that
A58: m1 in <^p2,p3^> by A56, 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
A59: [p2,p3] = [q2,q3] and
A60: <^q2,q3^> <> {} and
A61: <^q3,q2^> <> {} and
m1 = qq and
A62: qq is coretraction by A58;
[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
A63: [p1,p2] = [r1,r2] and
A64: <^r1,r2^> <> {} and
A65: <^r2,r1^> <> {} and
m2 = rr and
A66: rr is coretraction by A57;
A67: p2 = q2 by A59, XTUPLE_0:1;
then reconsider mm = qq as Morphism of r2,q3 by A63, XTUPLE_0:1;
A68: r2 = p2 by A63, XTUPLE_0:1;
A69: ex o1, o3 being Object of C ex m being Morphism of o1,o3 st
( [p1,p3] = [o1,o3] & <^o1,o3^> <> {} & <^o3,o1^> <> {} & mm * rr = m & m is coretraction )

proof

take r1 ; :: thesis:
take q3 ; :: thesis:
take mm * rr ; :: thesis:
p1 = r1 by A63, XTUPLE_0:1;
hence [p1,p3] = [r1,q3] by A59, XTUPLE_0:1; :: thesis:
thus A70: ( <^r1,q3^> <> {} & <^q3,r1^> <> {} ) by A60, A61, A64, A65, A68, A67, ALTCAT_1:def 2; :: thesis:
thus mm * rr = mm * rr ; :: thesis:
thus mm * rr is coretraction by A60, A62, A64, A66, A68, A67, A70, ALTCAT_3:19; :: 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 A69; :: 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:
A71: [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^> <> {} & <^o2,o1^> <> {} & m is coretraction ) ) :: thesis:

proof

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

end;

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