defpred S₁[ set , set ] means for x being set holds
( x in $2 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 iso ) );
set I = the carrier of C;
A1: for i being set st i in [: the carrier of C, the carrier of C:] holds
ex X being set st S₁[i,X]

let i be set ; :: thesis:
assume i in [: the carrier of C, the carrier of C:] ; :: thesis:
then consider o1, o2 being set 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₂[ 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) & S₂[x] ) ) from XBOOLE_0:sch 1();
take 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 iso ) ) :: 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 iso ) by A4;
take o1 ; :: thesis:
take o2 ; :: thesis:
take m ; :: thesis:
thus ( i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is iso ) 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 iso ) ; :: thesis:
( o1 = p1 & o2 = p2 ) by A3, A6, ZFMISC_1:27;
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 set st i in [: the carrier of C, the carrier of C:] holds
S₁[i,Ar . i] from PBOOLE:sch 3(A1);
defpred S₂[ 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)):] );
A9: for i being set st i in [: the carrier of C, the carrier of C, the carrier of C:] holds
ex j being set st S₂[i,j]

proof

let i be set ; :: thesis:
assume i in [: the carrier of C, the carrier of C, the carrier of C:] ; :: thesis:
then consider p1, p2, p3 being set 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 set 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 set ; :: according to TARSKI:def 3 :: thesis:
assume q in Ar . i ; :: thesis:
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 iso ) by A8, A14;
hence q in the Arrows of C . i ; :: thesis:

end;

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

proof

let i be set ; :: 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
A15: i = [p1,p2,p3] and
A16: Co . i = ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] by A12;
A17: [p1,p2] in [: the carrier of C, the carrier of C:] 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 [: 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, 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) = {} ; :: thesis:
assume [:(Ar . (p2,p3)),(Ar . (p1,p2)):] <> {} ; :: thesis:
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; :: thesis:

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 ; :: according to TARSKI:def 3 :: thesis:
assume q in rng f ; :: thesis:
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 [: the carrier of C, the carrier of C:] 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 [: the carrier of C, the carrier of C:] 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 ex 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, ZFMISC_1:27;
then reconsider mm = qq as Morphism of r2,q3 by A40, ZFMISC_1:27;
take r1 ; :: thesis:
take q3 ; :: thesis:
take mm * rr ; :: thesis:
A47: p1 = r1 by A40, ZFMISC_1:27;
hence [p1,p3] = [r1,q3] by A35, ZFMISC_1:27; :: thesis:
A48: r2 = p2 by A40, ZFMISC_1:27;
hence A49: ( <^r1,q3^> <> {} & <^q3,r1^> <> {} ) by A36, A37, A41, A42, A46, ALTCAT_1:def 2; :: thesis:
A50: p3 = q3 by A35, ZFMISC_1:27;
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 ; :: thesis:
thus mm * rr is iso by A36, A39, A41, A44, A48, A46, A49, ALTCAT_3:7; :: thesis:

end;

[p1,p3] in [: the carrier of C, the carrier of C:] by ZFMISC_1:def 2;
then q in Ar . [p1,p3] by A8, A45;
hence q in {|Ar|} . i by A15, A27, 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 A15, MULTOP_1:def 1;
hence Co . i is M2( bool [:({|Ar,Ar|} . i),({|Ar|} . i):]) by A23, A28, 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
A51: i = [p1,p2,p3] and
A52: Co . i = ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] by A12;
A53: ( 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 set ; :: 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 A52, A53;
hence q in the Comp of C . i by A51, 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
A54: <^p1,p2^> <> {} and
A55: <^p2,p3^> <> {} ; :: thesis:
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 [: the carrier of C, the carrier of C:] 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 [: the carrier of C, the carrier of C:] 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, ZFMISC_1:27;
then reconsider mm = qq as Morphism of r2,q3 by A62, ZFMISC_1:27;
A67: r2 = p2 by A62, ZFMISC_1:27;
A68: 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 iso )

proof

take r1 ; :: thesis:
take q3 ; :: thesis:
take mm * rr ; :: thesis:
p1 = r1 by A62, ZFMISC_1:27;
hence [p1,p3] = [r1,q3] by A58, ZFMISC_1:27; :: thesis:
thus A69: ( <^r1,q3^> <> {} & <^q3,r1^> <> {} ) by A59, A60, A63, A64, A67, A66, ALTCAT_1:def 2; :: thesis:
thus mm * rr = mm * rr ; :: thesis:
thus mm * rr is iso by A59, A61, A63, A65, A67, A66, A69, ALTCAT_3:7; :: thesis:

end;

[p1,p3] in [: the carrier of C, the carrier of C:] by ZFMISC_1:def 2;
hence not <^p1,p3^> = {} by A8, A68; :: 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:
A70: [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 iso ) ) :: thesis:

proof

assume m in the Arrows of IT . (o1,o2) ; :: thesis:
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, ZFMISC_1:27;
hence ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso ) by A72; :: thesis:

end;

assume ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso ) ; :: thesis:
hence m in the Arrows of IT . (o1,o2) by A8, A70; :: thesis: