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