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 ) )
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) ;

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

end;

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