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 ) )
( a in the carrier of (W -SUP(SO)_category ) & 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 ) ;

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

end;

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