let W be with_non-empty_element set ; 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); for f being set holds
( f in <^a,b^> iff f is infs-preserving Function of (latt a),(latt b) )
let f be set ; ( 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;
thus
( f is infs-preserving Function of (latt a),(latt b) implies f in <^a,b^> )
by A1, Def4; verum