let W be with_non-empty_element set ; :: thesis: for a, b being Object of (W -UPS_category)

for f being set holds

( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) )

let a, b be Object of (W -UPS_category); :: thesis: for f being set holds

( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) )

let f be set ; :: thesis: ( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) )

A1: ex w being non empty set st w in W by SETFAM_1:def 10;

for f being set holds

( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) )

let a, b be Object of (W -UPS_category); :: thesis: for f being set holds

( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) )

let f be set ; :: thesis: ( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) )

A1: ex w being non empty set st w in W by SETFAM_1:def 10;

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

thus
( f is directed-sups-preserving Function of (latt a),(latt b) implies f in <^a,b^> )
by A1, Def10; :: thesis: verumassume A2:
f in <^a,b^>
; :: thesis: f is directed-sups-preserving Function of (latt a),(latt b)

then reconsider g = f as Morphism of a,b ;

f = @ g by A2, Def7;

hence f is directed-sups-preserving Function of (latt a),(latt b) by A1, A2, Def10; :: thesis: verum

end;then reconsider g = f as Morphism of a,b ;

f = @ g by A2, Def7;

hence f is directed-sups-preserving Function of (latt a),(latt b) by A1, A2, Def10; :: thesis: verum