let W be with_non-empty_element set ; :: thesis: for a, b being LATTICE
for f being Function of a,b holds
( f in the Arrows of (W -SUP_category) . (a,b) iff ( a in the carrier of (W -SUP_category) & b in the carrier of (W -SUP_category) & a is complete & b is complete & f is sups-preserving ) )
A1: ex x being non empty set st x in W by SETFAM_1:def 10;
let a, b be LATTICE; :: thesis: for f being Function of a,b holds
( f in the Arrows of (W -SUP_category) . (a,b) iff ( a in the carrier of (W -SUP_category) & b in the carrier of (W -SUP_category) & a is complete & b is complete & f is sups-preserving ) )
let f be Function of a,b; :: thesis: ( f in the Arrows of (W -SUP_category) . (a,b) iff ( a in the carrier of (W -SUP_category) & b in the carrier of (W -SUP_category) & a is complete & b is complete & f is sups-preserving ) )
set A = W -SUP_category ;

hereby :: thesis: ( a in the carrier of (W -SUP_category) & b in the carrier of (W -SUP_category) & a is complete & b is complete & f is sups-preserving implies f in the Arrows of (W -SUP_category) . (a,b) )

assume f in the Arrows of (W -SUP_category) . (a,b) ; :: thesis: ( a in the carrier of (W -SUP_category) & b in the carrier of (W -SUP_category) & a is complete & b is complete & f is sups-preserving )
then consider o1, o2 being Object of (W -SUP_category) such that
A2: o1 = a and
A3: o2 = b and
A4: f in <^o1,o2^> and
f is Morphism of o1,o2 by Th12;
reconsider g = f as Morphism of o1,o2 by A4;
thus ( a in the carrier of (W -SUP_category) & b in the carrier of (W -SUP_category) ) by A2, A3; :: thesis: ( a is complete & b is complete & f is sups-preserving )
thus ( a is complete & b is complete ) by A1, A2, A3, Def5; :: thesis: f is sups-preserving
@ g = f by A4, YELLOW21:def 7;
hence f is sups-preserving by A1, A2, A3, A4, Def5; :: thesis: verum

end;

assume that
A5: a in the carrier of (W -SUP_category) and
A6: b in the carrier of (W -SUP_category) ; :: thesis: ( not a is complete or not b is complete or not f is sups-preserving or f in the Arrows of (W -SUP_category) . (a,b) )
reconsider x = a, y = b as Object of (W -SUP_category) by A5, A6;
A7: latt x = a ;
A8: latt y = b ;
assume that
a is complete and
b is complete and
A9: f is sups-preserving ; :: thesis: f in the Arrows of (W -SUP_category) . (a,b)
f in <^x,y^> by A1, A7, A8, A9, Def5;
hence f in the Arrows of (W -SUP_category) . (a,b) by ALTCAT_1:def 1; :: thesis: verum