thus F . p is Element of Funcs ((Valuations_in A),BOOLEAN) ; :: thesis: verum