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 -INF_category ) . a,b iff ( a in the carrier of (W -INF_category ) & b in the carrier of (W -INF_category ) & a is complete & b is complete & f is infs-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 -INF_category ) . a,b iff ( a in the carrier of (W -INF_category ) & b in the carrier of (W -INF_category ) & a is complete & b is complete & f is infs-preserving ) )
let f be Function of a,b; :: thesis: ( f in the Arrows of (W -INF_category ) . a,b iff ( a in the carrier of (W -INF_category ) & b in the carrier of (W -INF_category ) & a is complete & b is complete & f is infs-preserving ) )
set A = W -INF_category ;

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

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

end;

assume ( a in the carrier of (W -INF_category ) & b in the carrier of (W -INF_category ) ) ; :: thesis: ( not a is complete or not b is complete or not f is infs-preserving or f in the Arrows of (W -INF_category ) . a,b )
then reconsider x = a, y = b as object of (W -INF_category ) ;
A3: ( latt x = a & latt y = b ) ;
assume A4: ( a is complete & b is complete & f is infs-preserving ) ; :: thesis: f in the Arrows of (W -INF_category ) . a,b
f in <^x,y^> by A1, A3, A4, Def4;
hence f in the Arrows of (W -INF_category ) . a,b by ALTCAT_1:def 2; :: thesis: verum