let W be with_non-empty_element set ; :: thesis: for a, b being object of (W -CL-opp_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 -CL-opp_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 ) )
A1: a in the carrier of (W -CL-opp_category) ;
A2: b in the carrier of (W -CL-opp_category) ;
the carrier of (W -CL-opp_category) c= the carrier of (W -SUP(SO)_category) by ALTCAT_2:def 11;
then reconsider a1 = a, b1 = b as object of (W -SUP(SO)_category) by A1, A2;
<^a,b^> = <^a1,b1^> by ALTCAT_2:28;
hence ( 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 ) ) by Th50; :: thesis: verum