let W be with_non-empty_element set ; for a, b being Object of (W -SUP(SO)_category)
for f being set holds
( f in <^a,b^> iff ex g being sups-preserving Function of (latt a),(latt b) st
( g = f & UpperAdj g is directed-sups-preserving ) )
let a, b be Object of (W -SUP(SO)_category); for f being set holds
( f in <^a,b^> iff ex g being sups-preserving Function of (latt a),(latt b) st
( g = f & UpperAdj g is directed-sups-preserving ) )
let f be set ; ( f in <^a,b^> iff ex g being sups-preserving Function of (latt a),(latt b) st
( g = f & UpperAdj g is directed-sups-preserving ) )
the carrier of (W -SUP(SO)_category) c= the carrier of (W -SUP_category)
by ALTCAT_2:def 11;
then reconsider a1 = a, b1 = b as Object of (W -SUP_category) ;
hereby ( ex g being sups-preserving Function of (latt a),(latt b) st
( g = f & UpperAdj g is directed-sups-preserving ) implies f in <^a,b^> )
assume A1:
f in <^a,b^>
;
ex g being sups-preserving Function of (latt a),(latt b) st
( g = f & UpperAdj g is directed-sups-preserving )A2:
<^a,b^> c= <^a1,b1^>
by ALTCAT_2:31;
then reconsider g =
f as
Morphism of
a1,
b1 by A1;
A3:
f = @ g
by A1, A2, YELLOW21:def 7;
A4:
UpperAdj (@ g) is
directed-sups-preserving
by A1, A2, Def11;
f is
sups-preserving Function of
(latt a1),
(latt b1)
by A1, A2, Th16;
hence
ex
g being
sups-preserving Function of
(latt a),
(latt b) st
(
g = f &
UpperAdj g is
directed-sups-preserving )
by A3, A4;
verum
end;
given g being sups-preserving Function of (latt a),(latt b) such that A5:
g = f
and
A6:
UpperAdj g is directed-sups-preserving
; f in <^a,b^>
A7:
f in <^a1,b1^>
by A5, Th16;
reconsider g = f as Morphism of a1,b1 by A5, Th16;
f = @ g
by A7, YELLOW21:def 7;
hence
f in <^a,b^>
by A5, A6, A7, Def11; verum