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 & <^p1,p2^> <> {} holds
for n being Morphism of p1,p2 holds n is Morphism of 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 & <^p1,p2^> <> {} holds
for n being Morphism of p1,p2 holds n is Morphism of o1,o2
let o1, o2 be object of C; :: thesis: for p1, p2 being object of D st o1 = p1 & o2 = p2 & <^p1,p2^> <> {} holds
for n being Morphism of p1,p2 holds n is Morphism of o1,o2
let p1, p2 be object of D; :: thesis: ( o1 = p1 & o2 = p2 & <^p1,p2^> <> {} implies for n being Morphism of p1,p2 holds n is Morphism of o1,o2 )
assume that
A1: ( o1 = p1 & o2 = p2 ) and
A2: <^p1,p2^> <> {} ; :: thesis: for n being Morphism of p1,p2 holds n is Morphism of o1,o2
let n be Morphism of p1,p2; :: thesis: n is Morphism of o1,o2
A3: n in <^p1,p2^> by A2;
<^p1,p2^> c= <^o1,o2^> by A1, Th32;
hence n is Morphism of o1,o2 by A3; :: thesis: verum