let F, G be strict contravariant Functor of W -INF_category ,W -SUP_category ; :: thesis: ( ( for a being Object of (W -INF_category) holds F . a = latt a ) & ( for a, b being Object of (W -INF_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = LowerAdj (@ f) ) & ( for a being Object of (W -INF_category) holds G . a = latt a ) & ( for a, b being Object of (W -INF_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . f = LowerAdj (@ f) ) implies F = G )
assume that
A7: for a being Object of (W -INF_category) holds F . a = latt a and
A8: for a, b being Object of (W -INF_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = LowerAdj (@ f) and
A9: for a being Object of (W -INF_category) holds G . a = latt a and
A10: for a, b being Object of (W -INF_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . f = LowerAdj (@ f) ; :: thesis: F = G
A11: now :: thesis: for a being Object of (W -INF_category) holds F . a = G . a
let a be Object of (W -INF_category); :: thesis: F . a = G . a
thus F . a = latt a by A7
.= G . a by A9 ; :: thesis: verum
end;
now :: thesis: for a, b being Object of (W -INF_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = G . f
let a, b be Object of (W -INF_category); :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds F . f = G . f )
assume A12: <^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 = LowerAdj (@ f) by A8, A12
.= G . f by A10, A12 ; :: thesis: verum
end;
hence F = G by A11, YELLOW18:2; :: thesis: verum