let C be Category; 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; ( the carrier of C1 meets the carrier of C2 implies C1 /\ C2 = C2 /\ C1 )
assume
the carrier of C1 /\ the carrier of C2 <> {}
; XBOOLE_0:def 7 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; verum