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