let W be with_non-empty_element set ; :: thesis: for a, b being object of (W -CL_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 -CL_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) )
( a in the carrier of (W -CL_category ) & b in the carrier of (W -CL_category ) & the carrier of (W -CL_category ) c= the carrier of (W -INF(SC)_category ) ) by ALTCAT_2:def 11;
then reconsider a1 = a, b1 = b as object of (W -INF(SC)_category ) ;
<^a,b^> = <^a1,b1^> by ALTCAT_2:29;
hence ( f in <^a,b^> iff f is infs-preserving directed-sups-preserving Function of (latt a),(latt b) ) by Th48; :: thesis: verum