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^> <> {} & <^o2,o1^> <> {} & m is coretraction ) ) ) & 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^> <> {} & <^o2,o1^> <> {} & m is coretraction ) ) ) implies S1 = S2 )

assume that

A76: the carrier of S1 = the carrier of C and

A77: the Arrows of S1 cc= the Arrows of C and

A78: 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^> <> {} & <^o2,o1^> <> {} & m is coretraction ) ) and

A79: the carrier of S2 = the carrier of C and

A80: the Arrows of S2 cc= the Arrows of C and

A81: 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^> <> {} & <^o2,o1^> <> {} & m is coretraction ) ) ; :: thesis: S1 = S2

for m being Morphism of o1,o2 holds

( m in the Arrows of S1 . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is coretraction ) ) ) & 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^> <> {} & <^o2,o1^> <> {} & m is coretraction ) ) ) implies S1 = S2 )

assume that

A76: the carrier of S1 = the carrier of C and

A77: the Arrows of S1 cc= the Arrows of C and

A78: 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^> <> {} & <^o2,o1^> <> {} & m is coretraction ) ) and

A79: the carrier of S2 = the carrier of C and

A80: the Arrows of S2 cc= the Arrows of C and

A81: 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^> <> {} & <^o2,o1^> <> {} & m is coretraction ) ) ; :: 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

hence
S1 = S2
by A76, A79, ALTCAT_2:26, PBOOLE:3; :: thesis: verumthe 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 A82: 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

A83: ( o1 in the carrier of C & o2 in the carrier of C ) and

A84: i = [o1,o2] by ZFMISC_1:84;

reconsider o1 = o1, o2 = o2 as Object of C by A83;

thus the Arrows of S1 . i = the Arrows of S2 . i :: thesis: verum

end;assume A82: 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

A83: ( o1 in the carrier of C & o2 in the carrier of C ) and

A84: i = [o1,o2] by ZFMISC_1:84;

reconsider o1 = o1, o2 = o2 as Object of C by A83;

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

assume A88: 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 A79, A80, A82;

then reconsider m = n as Morphism of o1,o2 by A84, A88;

A89: m in the Arrows of S2 . (o1,o2) by A84, A88;

then A90: m is coretraction by A81;

( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) by A81, A89;

then m in the Arrows of S1 . (o1,o2) by A78, A90;

hence n in the Arrows of S1 . i by A84; :: thesis: verum

end;proof

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 )
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 A85: 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 A76, A77, A82;

then reconsider m = n as Morphism of o1,o2 by A84, A85;

A86: m in the Arrows of S1 . (o1,o2) by A84, A85;

then A87: m is coretraction by A78;

( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) by A78, A86;

then m in the Arrows of S2 . (o1,o2) by A81, A87;

hence n in the Arrows of S2 . i by A84; :: thesis: verum

end;assume A85: 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 A76, A77, A82;

then reconsider m = n as Morphism of o1,o2 by A84, A85;

A86: m in the Arrows of S1 . (o1,o2) by A84, A85;

then A87: m is coretraction by A78;

( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) by A78, A86;

then m in the Arrows of S2 . (o1,o2) by A81, A87;

hence n in the Arrows of S2 . i by A84; :: thesis: verum

assume A88: 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 A79, A80, A82;

then reconsider m = n as Morphism of o1,o2 by A84, A88;

A89: m in the Arrows of S2 . (o1,o2) by A84, A88;

then A90: m is coretraction by A81;

( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) by A81, A89;

then m in the Arrows of S1 . (o1,o2) by A78, A90;

hence n in the Arrows of S1 . i by A84; :: thesis: verum