let W be with_non-empty_element set ; :: thesis: W -INF(SC)_category = Intersect ((W -INF_category),(W -UPS_category))
consider w being non empty set such that
A1: w in W by SETFAM_1:def 10;
set r = the well-ordering upper-bounded Order of w;
A2: now :: thesis: for a being Object of (W -INF_category)
for b being Object of (W -UPS_category) st a = b holds
idm a = idm b
let a be Object of (W -INF_category); :: thesis: for b being Object of (W -UPS_category) st a = b holds
idm a = idm b
let b be Object of (W -UPS_category); :: thesis: ( a = b implies idm a = idm b )
idm a = id (latt a) by YELLOW21:2;
hence ( a = b implies idm a = idm b ) by YELLOW21:2; :: thesis: verum
end;
set B = Intersect ((W -INF_category),(W -UPS_category));
A3: W -INF_category ,W -UPS_category have_the_same_composition by YELLOW20:12;
then A4: the carrier of (Intersect ((W -INF_category),(W -UPS_category))) = the carrier of (W -INF_category) /\ the carrier of (W -UPS_category) by YELLOW20:def 3;
A5: RelStr(# w, the well-ordering upper-bounded Order of w #) is Object of (W -INF_category) by A1, Th13;
RelStr(# w, the well-ordering upper-bounded Order of w #) is Object of (W -UPS_category) by A1, YELLOW21:14;
then not Intersect ((W -INF_category),(W -UPS_category)) is empty by A4, A5, XBOOLE_0:def 4;
then reconsider I = Intersect ((W -INF_category),(W -UPS_category)) as non empty subcategory of W -INF_category by A2, YELLOW20:12, YELLOW20:25;
set A = W -INF(SC)_category ;
deffunc H1( set , set ) -> set = the Arrows of (W -INF(SC)_category) . ($1,$2);
A6: for C1, C2 being semi-functional para-functional category st the carrier of C1 = the carrier of (W -INF(SC)_category) & ( for a, b being Object of C1 holds <^a,b^> = H1(a,b) ) & the carrier of C2 = the carrier of (W -INF(SC)_category) & ( for a, b being Object of C2 holds <^a,b^> = H1(a,b) ) holds
AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #) from YELLOW18:sch 19();
 A7: the carrier of I = the carrier of (W -INF(SC)_category)
proof
thus the carrier of I c= the carrier of (W -INF(SC)_category) :: according to XBOOLE_0:def 10 :: thesis: the carrier of (W -INF(SC)_category) c= the carrier of I
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of I or x in the carrier of (W -INF(SC)_category) )
assume x in the carrier of I ; :: thesis: x in the carrier of (W -INF(SC)_category)
then reconsider x = x as Object of I ;
reconsider L = x as LATTICE by YELLOW21:def 4;
A8: x in the carrier of (W -UPS_category) by A4, XBOOLE_0:def 4;
then A9: ( L is strict & L is complete ) by A1, YELLOW21:def 10;
the carrier of L in W by A1, A8, YELLOW21:def 10;
then L is Object of (W -INF(SC)_category) by A9, Th43;
hence x in the carrier of (W -INF(SC)_category) ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (W -INF(SC)_category) or x in the carrier of I )
assume x in the carrier of (W -INF(SC)_category) ; :: thesis: x in the carrier of I
then reconsider x = x as Object of (W -INF(SC)_category) ;
reconsider L = x as LATTICE by YELLOW21:def 4;
A10: ( L is complete & L is strict ) by Th43;
A11: the carrier of L in W by Th43;
then A12: x is Object of (W -INF_category) by A10, Th13;
x is Object of (W -UPS_category) by A10, A11, YELLOW21:def 10;
hence x in the carrier of I by A4, A12, XBOOLE_0:def 4; :: thesis: verum
end;
A13: for a, b being Object of (W -INF(SC)_category) holds <^a,b^> = H1(a,b) by ALTCAT_1:def 1;
now :: thesis: for a, b being Object of I holds <^a,b^> = H1(a,b)
let a, b be Object of I; :: thesis: <^a,b^> = H1(a,b)
reconsider a9 = a, b9 = b as Object of (W -INF(SC)_category) by A7;
reconsider a1 = a, b1 = b as Object of (W -INF_category) by A4, XBOOLE_0:def 4;
reconsider a2 = a, b2 = b as Object of (W -UPS_category) by A4, XBOOLE_0:def 4;
A14: dom the Arrows of (W -INF_category) = [: the carrier of (W -INF_category), the carrier of (W -INF_category):] by PARTFUN1:def 2;
dom the Arrows of (W -UPS_category) = [: the carrier of (W -UPS_category), the carrier of (W -UPS_category):] by PARTFUN1:def 2;
then A15: (dom the Arrows of (W -INF_category)) /\ (dom the Arrows of (W -UPS_category)) = [:( the carrier of (W -INF_category) /\ the carrier of (W -UPS_category)),( the carrier of (W -INF_category) /\ the carrier of (W -UPS_category)):] by A14, ZFMISC_1:100;
A16: <^a,b^> = the Arrows of I . (a,b) by ALTCAT_1:def 1
.= (Intersect ( the Arrows of (W -INF_category), the Arrows of (W -UPS_category))) . [a,b] by A3, YELLOW20:def 3
.= ( the Arrows of (W -INF_category) . (a,b)) /\ ( the Arrows of (W -UPS_category) . [a,b]) by A4, A15, YELLOW20:def 2
.= <^a1,b1^> /\ ( the Arrows of (W -UPS_category) . (a,b)) by ALTCAT_1:def 1
.= <^a1,b1^> /\ <^a2,b2^> by ALTCAT_1:def 1 ;
now :: thesis: for f being object holds
( f in <^a,b^> iff f in H1(a,b) )
let f be object ; :: thesis: ( f in <^a,b^> iff f in H1(a,b) )
( f in <^a,b^> iff ( f in <^a1,b1^> & f in <^a2,b2^> ) ) by A16, XBOOLE_0:def 4;
then ( f in <^a,b^> iff ( f is directed-sups-preserving Function of (latt a2),(latt b2) & f is infs-preserving Function of (latt a1),(latt b1) ) ) by Th14, YELLOW21:15;
then ( f in <^a,b^> iff f in <^a9,b9^> ) by Th44;
hence ( f in <^a,b^> iff f in H1(a,b) ) by ALTCAT_1:def 1; :: thesis: verum
end;
hence <^a,b^> = H1(a,b) by TARSKI:2; :: thesis: verum
end;
hence W -INF(SC)_category = Intersect ((W -INF_category),(W -UPS_category)) by A6, A7, A13; :: thesis: verum