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) & latt a = a & idm b = id (latt b) & latt b = b ) by YELLOW21:2;
hence ( a = b implies idm a = idm b ) ; :: 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;
( RelStr(# w,r #) is object of (W -INF_category ) & RelStr(# w,r #) is object of (W -UPS_category ) ) by A1, Th13, YELLOW21:14;
then RelStr(# w,r #) in the carrier of (Intersect (W -INF_category ),(W -UPS_category )) by A4, XBOOLE_0:def 4;
then not Intersect (W -INF_category ),(W -UPS_category ) is empty ;
then reconsider I = Intersect (W -INF_category ),(W -UPS_category ) as non empty subcategory of W -INF_category by A2, A3, YELLOW20:26;
set A = W -INF(SC)_category ;
deffunc H₁( set , set ) -> set = the Arrows of (W -INF(SC)_category ) . $1,$2;
A5: 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();
A6: 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;
x in the carrier of (W -UPS_category ) by A4, XBOOLE_0:def 4;
then ( L is strict & L is complete & the carrier of L in W ) by A1, YELLOW21:def 10;
then L is object of (W -INF(SC)_category ) by 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;
( L is complete & L is strict & the carrier of L in W ) by Th47;
then ( x is object of (W -INF_category ) & x is object of (W -UPS_category ) ) by Th13, YELLOW21:def 10;
hence x in the carrier of I by A4, XBOOLE_0:def 4; :: thesis: verum

end;

A7: 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 a' = a, b' = b as object of (W -INF(SC)_category ) by A6;
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;
( dom the Arrows of (W -INF_category ) = [:the carrier of (W -INF_category ),the carrier of (W -INF_category ):] & dom the Arrows of (W -UPS_category ) = [:the carrier of (W -UPS_category ),the carrier of (W -UPS_category ):] ) by PARTFUN1:def 4;
then A8: ( (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 )):] & a in the carrier of I & b in the carrier of I ) by ZFMISC_1:123;
A9: <^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, A8, 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 A9, 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 <^a',b'^> ) 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 A5, A6, A7; :: thesis: verum