let A, B be AltCatStr ; :: thesis: ( A,B have_the_same_composition implies for a1, a2 being Object of A

for b1, b2 being Object of B

for o1, o2 being Object of (Intersect (A,B)) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 & <^a1,a2^> <> {} & <^b1,b2^> <> {} holds

for f being Morphism of a1,a2

for g being Morphism of b1,b2 st f = g holds

f in <^o1,o2^> )

assume A1: A,B have_the_same_composition ; :: thesis: for a1, a2 being Object of A

for b1, b2 being Object of B

for o1, o2 being Object of (Intersect (A,B)) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 & <^a1,a2^> <> {} & <^b1,b2^> <> {} holds

for f being Morphism of a1,a2

for g being Morphism of b1,b2 st f = g holds

f in <^o1,o2^>

let a1, a2 be Object of A; :: thesis: for b1, b2 being Object of B

for o1, o2 being Object of (Intersect (A,B)) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 & <^a1,a2^> <> {} & <^b1,b2^> <> {} holds

for f being Morphism of a1,a2

for g being Morphism of b1,b2 st f = g holds

f in <^o1,o2^>

let b1, b2 be Object of B; :: thesis: for o1, o2 being Object of (Intersect (A,B)) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 & <^a1,a2^> <> {} & <^b1,b2^> <> {} holds

for f being Morphism of a1,a2

for g being Morphism of b1,b2 st f = g holds

f in <^o1,o2^>

let o1, o2 be Object of (Intersect (A,B)); :: thesis: ( o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 & <^a1,a2^> <> {} & <^b1,b2^> <> {} implies for f being Morphism of a1,a2

for g being Morphism of b1,b2 st f = g holds

f in <^o1,o2^> )

assume ( o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 ) ; :: thesis: ( not <^a1,a2^> <> {} or not <^b1,b2^> <> {} or for f being Morphism of a1,a2

for g being Morphism of b1,b2 st f = g holds

f in <^o1,o2^> )

then <^o1,o2^> = <^a1,a2^> /\ <^b1,b2^> by A1, Th21;

hence ( not <^a1,a2^> <> {} or not <^b1,b2^> <> {} or for f being Morphism of a1,a2

for g being Morphism of b1,b2 st f = g holds

f in <^o1,o2^> ) by XBOOLE_0:def 4; :: thesis: verum

for b1, b2 being Object of B

for o1, o2 being Object of (Intersect (A,B)) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 & <^a1,a2^> <> {} & <^b1,b2^> <> {} holds

for f being Morphism of a1,a2

for g being Morphism of b1,b2 st f = g holds

f in <^o1,o2^> )

assume A1: A,B have_the_same_composition ; :: thesis: for a1, a2 being Object of A

for b1, b2 being Object of B

for o1, o2 being Object of (Intersect (A,B)) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 & <^a1,a2^> <> {} & <^b1,b2^> <> {} holds

for f being Morphism of a1,a2

for g being Morphism of b1,b2 st f = g holds

f in <^o1,o2^>

let a1, a2 be Object of A; :: thesis: for b1, b2 being Object of B

for o1, o2 being Object of (Intersect (A,B)) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 & <^a1,a2^> <> {} & <^b1,b2^> <> {} holds

for f being Morphism of a1,a2

for g being Morphism of b1,b2 st f = g holds

f in <^o1,o2^>

let b1, b2 be Object of B; :: thesis: for o1, o2 being Object of (Intersect (A,B)) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 & <^a1,a2^> <> {} & <^b1,b2^> <> {} holds

for f being Morphism of a1,a2

for g being Morphism of b1,b2 st f = g holds

f in <^o1,o2^>

let o1, o2 be Object of (Intersect (A,B)); :: thesis: ( o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 & <^a1,a2^> <> {} & <^b1,b2^> <> {} implies for f being Morphism of a1,a2

for g being Morphism of b1,b2 st f = g holds

f in <^o1,o2^> )

assume ( o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 ) ; :: thesis: ( not <^a1,a2^> <> {} or not <^b1,b2^> <> {} or for f being Morphism of a1,a2

for g being Morphism of b1,b2 st f = g holds

f in <^o1,o2^> )

then <^o1,o2^> = <^a1,a2^> /\ <^b1,b2^> by A1, Th21;

hence ( not <^a1,a2^> <> {} or not <^b1,b2^> <> {} or for f being Morphism of a1,a2

for g being Morphism of b1,b2 st f = g holds

f in <^o1,o2^> ) by XBOOLE_0:def 4; :: thesis: verum