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 = H1( 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 = H3( latt a, latt b, @ f) ) )
from YELLOW21:sch 7(A2, A1, A13, A14, A15, A16); verum