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:18; :: thesis: verum