let C be Category; :: thesis: for C1, C2 being Subcategory of C st the carrier of C1 meets the carrier of C2 holds
C1 /\ C2 = C2 /\ C1
let C1, C2 be Subcategory of C; :: thesis: ( the carrier of C1 meets the carrier of C2 implies C1 /\ C2 = C2 /\ C1 )
assume the carrier of C1 /\ the carrier of C2 <> {} ; :: according to XBOOLE_0:def 7 :: thesis: C1 /\ C2 = C2 /\ C1
then reconsider O = the carrier of C1 /\ the carrier of C2 as non empty set ;
consider o being Element of O;
set C12 = C1 /\ C2;
set C21 = C2 /\ C1;
set M1 = the carrier' of C1;
set M2 = the carrier' of C2;
set O1 = the carrier of C1;
set O2 = the carrier of C2;
A1: o is Object of C1 by XBOOLE_0:def 4;
A2: o is Object of C2 by XBOOLE_0:def 4;
then A3: the carrier of (C1 /\ C2) = O by A1, Def2;
A4: the carrier of (C2 /\ C1) = O by A1, A2, Def2;
A5: the carrier' of (C1 /\ C2) = the carrier' of C1 /\ the carrier' of C2 by A1, A2, Def2;
A6: the Source of (C2 /\ C1) = the Source of C2 | the carrier' of C1 by A1, A2, Def2;
A7: the Source of (C1 /\ C2) = the Source of C1 | the carrier' of C2 by A1, A2, Def2;
A8: the Target of (C2 /\ C1) = the Target of C2 | the carrier' of C1 by A1, A2, Def2;
A9: the Target of (C1 /\ C2) = the Target of C1 | the carrier' of C2 by A1, A2, Def2;
A10: the Id of (C2 /\ C1) = the Id of C2 | the carrier of C1 by A1, A2, Def2;
A11: the Id of (C1 /\ C2) = the Id of C1 | the carrier of C2 by A1, A2, Def2;
A12: the Comp of (C2 /\ C1) = the Comp of C2 || the carrier' of C1 by A1, A2, Def2;
A13: the Comp of (C1 /\ C2) = the Comp of C1 || the carrier' of C2 by A1, A2, Def2;
A14: the Source of C1 = the Source of C | the carrier' of C1 by NATTRA_1:8;
A15: the Target of C1 = the Target of C | the carrier' of C1 by NATTRA_1:8;
A16: the Source of C2 = the Source of C | the carrier' of C2 by NATTRA_1:8;
A17: the Target of C2 = the Target of C | the carrier' of C2 by NATTRA_1:8;
A18: the Source of (C1 /\ C2) = the Source of C | (the carrier' of C1 /\ the carrier' of C2) by A7, A14, RELAT_1:100
.= the Source of (C2 /\ C1) by A6, A16, RELAT_1:100 ;
A19: the Target of (C1 /\ C2) = the Target of C | (the carrier' of C1 /\ the carrier' of C2) by A9, A15, RELAT_1:100
.= the Target of (C2 /\ C1) by A8, A17, RELAT_1:100 ;
A20: the Comp of (C1 /\ C2) = (the Comp of C || the carrier' of C1) || the carrier' of C2 by A13, NATTRA_1:8
.= the Comp of C | ([:the carrier' of C1,the carrier' of C1:] /\ [:the carrier' of C2,the carrier' of C2:]) by RELAT_1:100
.= (the Comp of C || the carrier' of C2) || the carrier' of C1 by RELAT_1:100
.= the Comp of (C2 /\ C1) by A12, NATTRA_1:8 ;
the Id of (C1 /\ C2) = (the Id of C | the carrier of C1) | the carrier of C2 by A11, NATTRA_1:8
.= the Id of C | (the carrier of C1 /\ the carrier of C2) by RELAT_1:100
.= (the Id of C | the carrier of C2) | the carrier of C1 by RELAT_1:100
.= the Id of (C2 /\ C1) by A10, NATTRA_1:8 ;
hence C1 /\ C2 = C2 /\ C1 by A1, A2, A3, A4, A5, A18, A19, A20, Def2; :: thesis: verum