let S1, S2 be non empty transitive strict SubCatStr of C; ( 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
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 epi ) )
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 epi ) )
; S1 = S2
hence
S1 = S2
by A70, A73, ALTCAT_2:26, PBOOLE:3; verum