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
A49: the carrier of S1 = the carrier of C and
A50: the Arrows of S1 cc= the Arrows of C and
A51: 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
A52: the carrier of S2 = the carrier of C and
A53: the Arrows of S2 cc= the Arrows of C and
A54: 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

let i be set ; :: thesis: ( i in [:the carrier of C,the carrier of C:] implies the Arrows of S1 . i = the Arrows of S2 . i )
assume A55: 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 set such that
A56: ( o1 in the carrier of C & o2 in the carrier of C & i = [o1,o2] ) by ZFMISC_1:103;
reconsider o1 = o1, o2 = o2 as object of C by A56;
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 set ; :: according to TARSKI:def 3 :: thesis: ( not n in the Arrows of S1 . i or n in the Arrows of S2 . i )
assume A57: 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 A49, A50, A55, ALTCAT_2:def 2;
then reconsider m = n as Morphism of o1,o2 by A56, A57;
m in the Arrows of S1 . o1,o2 by A56, A57;
then ( <^o1,o2^> <> {} & m is mono ) by A51;
then m in the Arrows of S2 . o1,o2 by A54;
hence n in the Arrows of S2 . i by A56; :: thesis: verum

end;

let n be set ; :: according to TARSKI:def 3 :: thesis: ( not n in the Arrows of S2 . i or n in the Arrows of S1 . i )
assume A58: 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 A52, A53, A55, ALTCAT_2:def 2;
then reconsider m = n as Morphism of o1,o2 by A56, A58;
m in the Arrows of S2 . o1,o2 by A56, A58;
then ( <^o1,o2^> <> {} & m is mono ) by A54;
then m in the Arrows of S1 . o1,o2 by A51;
hence n in the Arrows of S1 . i by A56; :: thesis: verum

end;

end;

hence S1 = S2 by A49, A52, ALTCAT_2:27, PBOOLE:3; :: thesis: verum