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 ;
set o = the 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: the Element of O is Object of C1 by XBOOLE_0:def 4;
A2: the Element of 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 Comp of (C2 /\ C1) = the Comp of C2 || the carrier' of C1 by A1, A2, Def2;
A11: the Comp of (C1 /\ C2) = the Comp of C1 || the carrier' of C2 by A1, A2, Def2;
A12: the Source of C1 = the Source of C | the carrier' of C1 by NATTRA_1:8;
A13: the Target of C1 = the Target of C | the carrier' of C1 by NATTRA_1:8;
A14: the Source of C2 = the Source of C | the carrier' of C2 by NATTRA_1:8;
A15: the Target of C2 = the Target of C | the carrier' of C2 by NATTRA_1:8;
A16: the Source of (C1 /\ C2) = the Source of C | ( the carrier' of C1 /\ the carrier' of C2) by A7, A12, RELAT_1:71
.= the Source of (C2 /\ C1) by A6, A14, RELAT_1:71 ;
A17: the Target of (C1 /\ C2) = the Target of C | ( the carrier' of C1 /\ the carrier' of C2) by A9, A13, RELAT_1:71
.= the Target of (C2 /\ C1) by A8, A15, RELAT_1:71 ;
the Comp of (C1 /\ C2) = ( the Comp of C || the carrier' of C1) || the carrier' of C2 by A11, 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:71
.= ( the Comp of C || the carrier' of C2) || the carrier' of C1 by RELAT_1:71
.= the Comp of (C2 /\ C1) by A10, NATTRA_1:8 ;
hence C1 /\ C2 = C2 /\ C1 by A1, A2, A3, A4, A5, A16, A17, Def2; :: thesis: verum