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

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