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 ) )
A1: (W LowerAdj ) " = W UpperAdj by Th18;
(W UpperAdj ) " = W LowerAdj by Th18;
hence ( (W LowerAdj ) * (W UpperAdj ) = id (W -SUP_category ) & (W UpperAdj ) * (W LowerAdj ) = id (W -INF_category ) ) by A1, FUNCTOR1:21; :: thesis: verum