let W be with_non-empty_element set ; :: thesis: ( (W LowerAdj ) * (W UpperAdj ) = id (W -SUP_category ) & (W UpperAdj ) * (W LowerAdj ) = id (W -INF_category ) )
( (W LowerAdj ) " = W UpperAdj & (W UpperAdj ) " = W LowerAdj ) by Th18;
hence ( (W LowerAdj ) * (W UpperAdj ) = id (W -SUP_category ) & (W UpperAdj ) * (W LowerAdj ) = id (W -INF_category ) ) by FUNCTOR1:21; :: thesis: verum