let W be with_non-empty_element set ; :: thesis: for a, b being Object of (W -ALG_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 -ALG_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) )

reconsider a1 = a, b1 = b as Object of (W -CONT_category) by ALTCAT_2:29;

<^a,b^> = <^a1,b1^> by ALTCAT_2:28;

hence ( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) ) by Th18; :: thesis: verum

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

reconsider a1 = a, b1 = b as Object of (W -CONT_category) by ALTCAT_2:29;

<^a,b^> = <^a1,b1^> by ALTCAT_2:28;

hence ( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) ) by Th18; :: thesis: verum