let W be with_non-empty_element set ; :: thesis: for a, b being Object of (W -INF(SC)_category)
for f being set holds
( f in <^a,b^> iff f is infs-preserving directed-sups-preserving Function of (latt a),(latt b) )
let a, b be Object of (W -INF(SC)_category); :: thesis: for f being set holds
( f in <^a,b^> iff f is infs-preserving directed-sups-preserving Function of (latt a),(latt b) )
let f be set ; :: thesis: ( f in <^a,b^> iff f is infs-preserving directed-sups-preserving Function of (latt a),(latt b) )
the carrier of (W -INF(SC)_category) c= the carrier of (W -INF_category) by ALTCAT_2:def 11;
then reconsider a1 = a, b1 = b as Object of (W -INF_category) ;

hereby :: thesis: ( f is infs-preserving directed-sups-preserving Function of (latt a),(latt b) implies f in <^a,b^> )

assume A1: f in <^a,b^> ; :: thesis: f is infs-preserving directed-sups-preserving Function of (latt a),(latt b)
A2: <^a,b^> c= <^a1,b1^> by ALTCAT_2:31;
then reconsider g = f as Morphism of a1,b1 by A1;
f = @ g by A1, A2, YELLOW21:def 7;
hence f is infs-preserving directed-sups-preserving Function of (latt a),(latt b) by A1, A2, Def10, Th14; :: thesis: verum

end;

assume f is infs-preserving directed-sups-preserving Function of (latt a),(latt b) ; :: thesis: f in <^a,b^>
then reconsider f = f as infs-preserving directed-sups-preserving Function of (latt a),(latt b) ;
A3: f in <^a1,b1^> by Th14;
reconsider g = f as Morphism of a1,b1 by Th14;
f = @ g by A3, YELLOW21:def 7;
hence f in <^a,b^> by A3, Def10; :: thesis: verum