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