let W be with_non-empty_element set ; :: thesis: for a, b being object of (W -SUP(SO)_category)
for f being set holds
( f in <^a,b^> iff ex g being sups-preserving Function of (latt a),(latt b) st
( g = f & UpperAdj g is directed-sups-preserving ) )
let a, b be object of (W -SUP(SO)_category); :: thesis: for f being set holds
( f in <^a,b^> iff ex g being sups-preserving Function of (latt a),(latt b) st
( g = f & UpperAdj g is directed-sups-preserving ) )
let f be set ; :: thesis: ( f in <^a,b^> iff ex g being sups-preserving Function of (latt a),(latt b) st
( g = f & UpperAdj g is directed-sups-preserving ) )
A1: a in the carrier of (W -SUP(SO)_category) ;
A2: b in the carrier of (W -SUP(SO)_category) ;
the carrier of (W -SUP(SO)_category) c= the carrier of (W -SUP_category) by ALTCAT_2:def 11;
then reconsider a1 = a, b1 = b as object of (W -SUP_category) by A1, A2;

hereby :: thesis: ( ex g being sups-preserving Function of (latt a),(latt b) st
( g = f & UpperAdj g is directed-sups-preserving ) implies f in <^a,b^> )

assume A3: f in <^a,b^> ; :: thesis: ex g being sups-preserving Function of (latt a),(latt b) st
( g = f & UpperAdj g is directed-sups-preserving )
A4: <^a,b^> c= <^a1,b1^> by ALTCAT_2:31;
then reconsider g = f as Morphism of a1,b1 by A3;
A5: f = @ g by A3, A4, YELLOW21:def 7;
A6: UpperAdj (@ g) is directed-sups-preserving by A3, A4, Def11;
f is sups-preserving Function of (latt a1),(latt b1) by A3, A4, Th16;
hence ex g being sups-preserving Function of (latt a),(latt b) st
( g = f & UpperAdj g is directed-sups-preserving ) by A5, A6; :: thesis: verum

end;

given g being sups-preserving Function of (latt a),(latt b) such that A7: g = f and
A8: UpperAdj g is directed-sups-preserving ; :: thesis: f in <^a,b^>
A9: f in <^a1,b1^> by A7, Th16;
reconsider g = f as Morphism of a1,b1 by A7, Th16;
f = @ g by A9, YELLOW21:def 7;
hence f in <^a,b^> by A7, A8, A9, Def11; :: thesis: verum