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 A1: ( o1 = p1 & o2 = p2 & <^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
( n in <^p1,p2^> & <^p1,p2^> c= <^o1,o2^> ) by A1, Th31;
hence n is Morphism of o1,o2 ; :: thesis: verum