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 <> {}
;
A3:
C1 /\ C2 = C2 /\ C1
by A1, Th5;
now for C1, C2 being Subcategory of C st the carrier of C1 /\ the carrier of C2 <> {} holds
C1 /\ C2 is Subcategory of C1let 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
Source of
C1 = the
Source of
C1 | (dom the Source of C1)
;
dom the
Source of
C1 = the
carrier' of
C1
by FUNCT_2:def 1;
then A15:
the
Source of
(C1 /\ C2) = the
Source of
C1 | the
carrier' of
(C1 /\ C2)
by A10, A11, A14, RELAT_1:71;
A16:
the
Target of
C1 = the
Target of
C1 | (dom the Target of C1)
;
dom the
Target of
C1 = the
carrier' of
C1
by FUNCT_2:def 1;
then A17:
the
Target of
(C1 /\ C2) = the
Target of
C1 | the
carrier' of
(C1 /\ C2)
by A10, A12, A16, RELAT_1:71;
A18:
for
o being
Element of
C1 st
o in O holds
id o in the
carrier' of
C1 /\ the
carrier' of
C2
the
Comp of
C1 = the
Comp of
C1 || the
carrier' of
C1
;
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, A15, A17, A18, NATTRA_1:9;
verum end;
hence
( C1 /\ C2 is Subcategory of C1 & C1 /\ C2 is Subcategory of C2 )
by A2, A3; verum