let W be with_non-empty_element set ; 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; 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; ( 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 ( 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)
;
( 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;
( a is complete & b is complete & f is sups-preserving )thus
(
a is
complete &
b is
complete )
by A1, A2, A3, Def5;
f is sups-preserving
@ g = f
by A4, YELLOW21:def 7;
hence
f is
sups-preserving
by A1, A2, A3, A4, Def5;
verum
end;
assume that
A5:
a in the carrier of (W -SUP_category)
and
A6:
b in the carrier of (W -SUP_category)
; ( 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
; 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; verum