set A = W -SUP_category ;
set B = W -INF_category ;
set F = W UpperAdj ;
A24: ex x being non empty set st x in W by SETFAM_1:def 10;
deffunc H1( Object of (W -SUP_category)) -> RelStr = latt W;
deffunc H2( Object of (W -SUP_category), Object of (W -SUP_category), Morphism of W,c2) -> Function of (latt c2),(latt W) = UpperAdj (@ c3);
A25: for a being Object of (W -SUP_category) holds (W UpperAdj) . a = H1(a) by Def7;
A26: for a, b being Object of (W -SUP_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds (W UpperAdj) . f = H2(a,b,f) by Def7;
A27: for a, b being Object of (W -SUP_category) st H1(a) = H1(b) holds
a = b ;
A28: now :: thesis: for a, b being Object of (W -SUP_category) st <^a,b^> <> {} holds
for f, g being Morphism of a,b st H2(a,b,f) = H2(a,b,g) holds
f = g
let a, b be Object of (W -SUP_category); :: thesis: ( <^a,b^> <> {} implies for f, g being Morphism of a,b st H2(a,b,f) = H2(a,b,g) holds
f = g )
assume A29: <^a,b^> <> {} ; :: thesis: for f, g being Morphism of a,b st H2(a,b,f) = H2(a,b,g) holds
f = g
let f, g be Morphism of a,b; :: thesis: ( H2(a,b,f) = H2(a,b,g) implies f = g )
A30: @ f = f by A29, YELLOW21:def 7;
A31: @ g = g by A29, YELLOW21:def 7;
A32: latt a is complete ;
A33: latt b is complete ;
A34: @ f is sups-preserving by A24, A29, A30, Def5;
A35: @ g is sups-preserving by A24, A29, A31, Def5;
assume H2(a,b,f) = H2(a,b,g) ; :: thesis: f = g
hence f = LowerAdj (UpperAdj (@ g)) by A30, A32, A33, A34, Th11
.= g by A31, A32, A33, A35, Th11 ;
:: thesis: verum
end;
A36: now :: thesis: for a, b being Object of (W -INF_category) st <^a,b^> <> {} holds
for f being Morphism of a,b ex c, d being Object of (W -SUP_category) ex g being Morphism of c,d st
( b = H1(c) & a = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) )
let a, b be Object of (W -INF_category); :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b ex c, d being Object of (W -SUP_category) ex g being Morphism of c,d st
( b = H1(c) & a = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) ) )
assume A37: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b ex c, d being Object of (W -SUP_category) ex g being Morphism of c,d st
( b = H1(c) & a = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) )
let f be Morphism of a,b; :: thesis: ex c, d being Object of (W -SUP_category) ex g being Morphism of c,d st
( b = H1(c) & a = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) )
A38: ( latt a is strict & latt a is complete ) by A24, Def4;
A39: the carrier of (latt a) in W by A24, Def4;
A40: ( latt b is strict & latt b is complete ) by A24, Def4;
the carrier of (latt b) in W by A24, Def4;
then reconsider c = latt b, d = latt a as Object of (W -SUP_category) by A38, A39, A40, Def5;
take c = c; :: thesis: ex d being Object of (W -SUP_category) ex g being Morphism of c,d st
( b = H1(c) & a = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) )
take d = d; :: thesis: ex g being Morphism of c,d st
( b = H1(c) & a = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) )
A41: latt c = c ;
A42: latt d = d ;
A43: f = @ f by A37, YELLOW21:def 7;
then A44: @ f is infs-preserving by A24, A37, Def4;
then A45: ( LowerAdj (@ f) is monotone & LowerAdj (@ f) is sups-preserving ) by A41, A42;
A46: LowerAdj (@ f) in <^c,d^> by A24, A44, Def5;
reconsider g = LowerAdj (@ f) as Morphism of c,d by A24, A44, Def5;
take g = g; :: thesis: ( b = H1(c) & a = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) )
thus ( b = H1(c) & a = H1(d) & <^c,d^> <> {} ) by A24, A45, Def5; :: thesis: f = H2(c,d,g)
g = @ g by A46, YELLOW21:def 7;
hence f = H2(c,d,g) by A43, A44, Th10; :: thesis: verum
end;
thus W UpperAdj is bijective from YELLOW18:sch 12(A25, A26, A27, A28, A36); :: thesis: verum