let S1, S2 be non empty transitive strict SubCatStr of C; :: thesis: ( the carrier of S1 = the carrier of C & the Arrows of S1 cc= the Arrows of C & ( for o1, o2 being Object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of S1 . (o1,o2) iff ( <^o1,o2^> <> {} & m is mono ) ) ) & the carrier of S2 = the carrier of C & the Arrows of S2 cc= the Arrows of C & ( for o1, o2 being Object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of S2 . (o1,o2) iff ( <^o1,o2^> <> {} & m is mono ) ) ) implies S1 = S2 )
assume that
A70: the carrier of S1 = the carrier of C and
A71: the Arrows of S1 cc= the Arrows of C and
A72: for o1, o2 being Object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of S1 . (o1,o2) iff ( <^o1,o2^> <> {} & m is mono ) ) and
A73: the carrier of S2 = the carrier of C and
A74: the Arrows of S2 cc= the Arrows of C and
A75: for o1, o2 being Object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of S2 . (o1,o2) iff ( <^o1,o2^> <> {} & m is mono ) ) ; :: thesis: S1 = S2

now :: thesis: for i being object st i in [: the carrier of C, the carrier of C:] holds
the Arrows of S1 . i = the Arrows of S2 . i

let i be object ; :: thesis: ( i in [: the carrier of C, the carrier of C:] implies the Arrows of S1 . i = the Arrows of S2 . i )
assume A76: i in [: the carrier of C, the carrier of C:] ; :: thesis: the Arrows of S1 . i = the Arrows of S2 . i
then consider o1, o2 being object such that
A77: ( o1 in the carrier of C & o2 in the carrier of C ) and
A78: i = [o1,o2] by ZFMISC_1:84;
reconsider o1 = o1, o2 = o2 as Object of C by A77;
thus the Arrows of S1 . i = the Arrows of S2 . i :: thesis: verum

proof

thus the Arrows of S1 . i c= the Arrows of S2 . i :: according to XBOOLE_0:def 10 :: thesis: the Arrows of S2 . i c= the Arrows of S1 . i

proof

let n be object ; :: according to TARSKI:def 3 :: thesis: ( not n in the Arrows of S1 . i or n in the Arrows of S2 . i )
assume A79: n in the Arrows of S1 . i ; :: thesis: n in the Arrows of S2 . i
the Arrows of S1 . i c= the Arrows of C . i by A70, A71, A76;
then reconsider m = n as Morphism of o1,o2 by A78, A79;
m in the Arrows of S1 . (o1,o2) by A78, A79;
then ( <^o1,o2^> <> {} & m is mono ) by A72;
then m in the Arrows of S2 . (o1,o2) by A75;
hence n in the Arrows of S2 . i by A78; :: thesis: verum

end;

let n be object ; :: according to TARSKI:def 3 :: thesis: ( not n in the Arrows of S2 . i or n in the Arrows of S1 . i )
assume A80: n in the Arrows of S2 . i ; :: thesis: n in the Arrows of S1 . i
the Arrows of S2 . i c= the Arrows of C . i by A73, A74, A76;
then reconsider m = n as Morphism of o1,o2 by A78, A80;
m in the Arrows of S2 . (o1,o2) by A78, A80;
then ( <^o1,o2^> <> {} & m is mono ) by A75;
then m in the Arrows of S1 . (o1,o2) by A72;
hence n in the Arrows of S1 . i by A78; :: thesis: verum

end;

end;

hence S1 = S2 by A70, A73, ALTCAT_2:26, PBOOLE:3; :: thesis: verum