let a be Object of (W -SUP_category); :: thesis: ( S₁[a] implies S₂[a,a, idm a] )
A13: idm a = id (latt a) by YELLOW21:2;
UpperAdj (id (latt a)) = id (latt a) by Th7;
hence ( S₁[a] implies S₂[a,a, idm a] ) by A13, YELLOW21:def 7; :: thesis: verum