consider a being Element of E such that
A: E == FAdj (F,{a}) by defsimp;
take a ; :: thesis: a is F -primitive
thus a is F -primitive by A; :: thesis: verum