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 epi ) ) ) & 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 epi ) ) ) implies S1 = S2 )
assume that
A67: the carrier of S1 = the carrier of C and
A68: the Arrows of S1 cc= the Arrows of C and
A69: 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 epi ) ) and
A70: the carrier of S2 = the carrier of C and
A71: the Arrows of S2 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 S2 . (o1,o2) iff ( <^o1,o2^> <> {} & m is epi ) ) ; :: 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 A73: 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
A74: ( o1 in the carrier of C & o2 in the carrier of C ) and
A75: i = [o1,o2] by ZFMISC_1:84;
reconsider o1 = o1, o2 = o2 as object of C by A74;
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 A76: 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 A67, A68, A73, ALTCAT_2:def 2;
then reconsider m = n as Morphism of o1,o2 by A75, A76;
m in the Arrows of S1 . (o1,o2) by A75, A76;
then ( <^o1,o2^> <> {} & m is epi ) by A69;
then m in the Arrows of S2 . (o1,o2) by A72;
hence n in the Arrows of S2 . i by A75; :: 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 A77: 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 A70, A71, A73, ALTCAT_2:def 2;
then reconsider m = n as Morphism of o1,o2 by A75, A77;
m in the Arrows of S2 . (o1,o2) by A75, A77;
then ( <^o1,o2^> <> {} & m is epi ) by A72;
then m in the Arrows of S1 . (o1,o2) by A69;
hence n in the Arrows of S1 . i by A75; :: thesis: verum

end;

end;

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