let F, G be strict contravariant Functor of W -SUP_category ,W -INF_category ; :: thesis: ( ( for a being object of (W -SUP_category ) holds F . a = latt a ) & ( for a, b being object of (W -SUP_category ) st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = UpperAdj (@ f) ) & ( for a being object of (W -SUP_category ) holds G . a = latt a ) & ( for a, b being object of (W -SUP_category ) st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . f = UpperAdj (@ f) ) implies F = G )
assume that
A17: for a being object of (W -SUP_category ) holds F . a = latt a and
A18: for a, b being object of (W -SUP_category ) st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = UpperAdj (@ f) and
A19: for a being object of (W -SUP_category ) holds G . a = latt a and
A20: for a, b being object of (W -SUP_category ) st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . f = UpperAdj (@ f) ; :: thesis: F = G

A21: now

let a be object of (W -SUP_category ); :: thesis: F . a = G . a
thus F . a = latt a by A17
.= G . a by A19 ; :: thesis: verum

end;

now

let a, b be object of (W -SUP_category ); :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds F . f = G . f )
assume A22: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b holds F . f = G . f
let f be Morphism of a,b; :: thesis: F . f = G . f
thus F . f = UpperAdj (@ f) by A18, A22
.= G . f by A20, A22 ; :: thesis: verum

end;

hence F = G by A21, YELLOW18:2; :: thesis: verum