let C be non empty AltCatStr ; :: thesis: for D being non empty SubCatStr of C
for o1, o2 being Object of C
for p1, p2 being Object of D st o1 = p1 & o2 = p2 holds
<^p1,p2^> c= <^o1,o2^>
let D be non empty SubCatStr of C; :: thesis: for o1, o2 being Object of C
for p1, p2 being Object of D st o1 = p1 & o2 = p2 holds
<^p1,p2^> c= <^o1,o2^>
let o1, o2 be Object of C; :: thesis: for p1, p2 being Object of D st o1 = p1 & o2 = p2 holds
<^p1,p2^> c= <^o1,o2^>
let p1, p2 be Object of D; :: thesis: ( o1 = p1 & o2 = p2 implies <^p1,p2^> c= <^o1,o2^> )
assume A1: ( o1 = p1 & o2 = p2 ) ; :: thesis: <^p1,p2^> c= <^o1,o2^>
( [p1,p2] in [: the carrier of D, the carrier of D:] & the Arrows of D cc= the Arrows of C ) by Def11;
hence <^p1,p2^> c= <^o1,o2^> by A1; :: thesis: verum