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 11;
consider r being well-ordering upper-bounded Order of w;

A2: now

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,r #) is object of (W -INF_category ) by A1, Th13;
RelStr(# w,r #) 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:26;
set A = W -INF(SC)_category ;
deffunc H₁( 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^> = H₁(a,b) ) & the carrier of C2 = the carrier of (W -INF(SC)_category ) & ( for a, b being object of C2 holds <^a,b^> = H₁(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 set ; :: 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, Th47;
hence x in the carrier of (W -INF(SC)_category ) ; :: thesis: verum

end;

let x be set ; :: 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 Th47;
A11: the carrier of L in W by Th47;
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^> = H₁(a,b) by ALTCAT_1:def 2;

now

let a, b be object of I; :: thesis: <^a,b^> = H₁(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 4;
dom the Arrows of (W -UPS_category ) = [:the carrier of (W -UPS_category ),the carrier of (W -UPS_category ):] by PARTFUN1:def 4;
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:123;
A16: <^a,b^> = the Arrows of I . a,b by ALTCAT_1:def 2
.= (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 2
.= <^a1,b1^> /\ <^a2,b2^> by ALTCAT_1:def 2 ;

now

let f be set ; :: thesis: ( f in <^a,b^> iff f in H₁(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 Th48;
hence ( f in <^a,b^> iff f in H₁(a,b) ) by ALTCAT_1:def 2; :: thesis: verum

end;

hence <^a,b^> = H₁(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