let W be with_non-empty_element set ; for a, b being Object of (W -INF(SC)_category)
for f being set holds
( f in <^a,b^> iff f is infs-preserving directed-sups-preserving Function of (latt a),(latt b) )
let a, b be Object of (W -INF(SC)_category); for f being set holds
( f in <^a,b^> iff f is infs-preserving directed-sups-preserving Function of (latt a),(latt b) )
let f be set ; ( f in <^a,b^> iff f is infs-preserving directed-sups-preserving Function of (latt a),(latt b) )
the carrier of (W -INF(SC)_category) c= the carrier of (W -INF_category)
by ALTCAT_2:def 11;
then reconsider a1 = a, b1 = b as Object of (W -INF_category) ;
hereby ( f is infs-preserving directed-sups-preserving Function of (latt a),(latt b) implies f in <^a,b^> )
assume A1:
f in <^a,b^>
;
f is infs-preserving directed-sups-preserving Function of (latt a),(latt b)A2:
<^a,b^> c= <^a1,b1^>
by ALTCAT_2:31;
then reconsider g =
f as
Morphism of
a1,
b1 by A1;
f = @ g
by A1, A2, YELLOW21:def 7;
hence
f is
infs-preserving directed-sups-preserving Function of
(latt a),
(latt b)
by A1, A2, Def10, Th14;
verum
end;
assume
f is infs-preserving directed-sups-preserving Function of (latt a),(latt b)
; f in <^a,b^>
then reconsider f = f as infs-preserving directed-sups-preserving Function of (latt a),(latt b) ;
A3:
f in <^a1,b1^>
by Th14;
reconsider g = f as Morphism of a1,b1 by Th14;
f = @ g
by A3, YELLOW21:def 7;
hence
f in <^a,b^>
by A3, Def10; verum