let W be with_non-empty_element set ; :: thesis: for a, b being Object of (W -INF_category)
for f being set holds
( f in <^a,b^> iff f is infs-preserving Function of (latt a),(latt b) )
let a, b be Object of (W -INF_category); :: thesis: for f being set holds
( f in <^a,b^> iff f is infs-preserving Function of (latt a),(latt b) )
let f be set ; :: thesis: ( f in <^a,b^> iff f is infs-preserving Function of (latt a),(latt b) )
A1: ex a being non empty set st a in W by SETFAM_1:def 10;
hereby :: thesis: ( f is infs-preserving Function of (latt a),(latt b) implies f in <^a,b^> )
assume A2: f in <^a,b^> ; :: thesis: f is infs-preserving Function of (latt a),(latt b)
then reconsider g = f as Morphism of a,b ;
f = @ g by A2, YELLOW21:def 7;
hence f is infs-preserving Function of (latt a),(latt b) by A1, A2, Def4; :: thesis: verum
end;
thus ( f is infs-preserving Function of (latt a),(latt b) implies f in <^a,b^> ) by A1, Def4; :: thesis: verum