let C be Category; for C1, C2 being Subcategory of C st the carrier of C1 meets the carrier of C2 holds
( C1 /\ C2 is Subcategory of C1 & C1 /\ C2 is Subcategory of C2 )
let C1, C2 be Subcategory of C; ( the carrier of C1 meets the carrier of C2 implies ( C1 /\ C2 is Subcategory of C1 & C1 /\ C2 is Subcategory of C2 ) )
assume A1:
the carrier of C1 meets the carrier of C2
; ( C1 /\ C2 is Subcategory of C1 & C1 /\ C2 is Subcategory of C2 )
then A2:
the carrier of C1 /\ the carrier of C2 <> {}
by XBOOLE_0:def 7;
A3:
C1 /\ C2 = C2 /\ C1
by A1, Th5;
now let C1,
C2 be
Subcategory of
C;
( the carrier of C1 /\ the carrier of C2 <> {} implies C1 /\ C2 is Subcategory of C1 )assume A4:
the
carrier of
C1 /\ the
carrier of
C2 <> {}
;
C1 /\ C2 is Subcategory of C1A5:
the
carrier of
C1 /\ the
carrier of
C2 c= the
carrier of
C1
by XBOOLE_1:17;
A6:
the
carrier' of
C1 /\ the
carrier' of
C2 c= the
carrier' of
C1
by XBOOLE_1:17;
reconsider O = the
carrier of
C1 /\ the
carrier of
C2 as non
empty set by A4;
set o = the
Element of
O;
A7:
the
Element of
O is
Object of
C1
by XBOOLE_0:def 4;
A8:
the
Element of
O is
Object of
C2
by XBOOLE_0:def 4;
then A9:
the
carrier of
(C1 /\ C2) = the
carrier of
C1 /\ the
carrier of
C2
by A7, Def2;
A10:
the
carrier' of
(C1 /\ C2) = the
carrier' of
C1 /\ the
carrier' of
C2
by A7, A8, Def2;
A11:
the
Source of
(C1 /\ C2) = the
Source of
C1 | the
carrier' of
C2
by A7, A8, Def2;
A12:
the
Target of
(C1 /\ C2) = the
Target of
C1 | the
carrier' of
C2
by A7, A8, Def2;
A13:
the
Comp of
(C1 /\ C2) = the
Comp of
C1 || the
carrier' of
C2
by A7, A8, Def2;
A14:
the
Id of
(C1 /\ C2) = the
Id of
C1 | the
carrier of
C2
by A7, A8, Def2;
A15:
the
Source of
C1 = the
Source of
C1 | (dom the Source of C1)
by RELAT_1:68;
dom the
Source of
C1 = the
carrier' of
C1
by FUNCT_2:def 1;
then A16:
the
Source of
(C1 /\ C2) = the
Source of
C1 | the
carrier' of
(C1 /\ C2)
by A10, A11, A15, RELAT_1:71;
A17:
the
Target of
C1 = the
Target of
C1 | (dom the Target of C1)
by RELAT_1:68;
dom the
Target of
C1 = the
carrier' of
C1
by FUNCT_2:def 1;
then A18:
the
Target of
(C1 /\ C2) = the
Target of
C1 | the
carrier' of
(C1 /\ C2)
by A10, A12, A17, RELAT_1:71;
A19:
the
Id of
C1 = the
Id of
C1 | (dom the Id of C1)
by RELAT_1:68;
dom the
Id of
C1 = the
carrier of
C1
by FUNCT_2:def 1;
then A20:
the
Id of
(C1 /\ C2) = the
Id of
C1 | the
carrier of
(C1 /\ C2)
by A9, A14, A19, RELAT_1:71;
dom the
Comp of
C1 c= [: the carrier' of C1, the carrier' of C1:]
;
then
the
Comp of
C1 = the
Comp of
C1 || the
carrier' of
C1
by RELAT_1:68;
then
the
Comp of
(C1 /\ C2) = the
Comp of
C1 | ([: the carrier' of C1, the carrier' of C1:] /\ [: the carrier' of C2, the carrier' of C2:])
by A13, RELAT_1:71;
then
the
Comp of
(C1 /\ C2) = the
Comp of
C1 || the
carrier' of
(C1 /\ C2)
by A10, ZFMISC_1:100;
hence
C1 /\ C2 is
Subcategory of
C1
by A5, A6, A9, A10, A16, A18, A20, NATTRA_1:9;
verum end;
hence
( C1 /\ C2 is Subcategory of C1 & C1 /\ C2 is Subcategory of C2 )
by A2, A3; verum