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