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 11;
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 2; :: thesis: verum