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) )
A1: a in the carrier of (W -INF(SC)_category) ;
A2: b in the carrier of (W -INF(SC)_category) ;
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) by A1, A2;

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

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