thus ex F being strict contravariant Functor of W -SUP_category ,W -INF_category st
( ( for a being Object of (W -SUP_category) holds F . a = H₁( 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 = H₃( latt a, latt b, @ f) ) ) from YELLOW21:sch 7(A2, A1, A13, A14, A15, A16); :: thesis: verum