ModelSP S c= Funcs S,BOOLEAN ;
hence ModelSP S is non empty Subset of (Funcs S,BOOLEAN ) ; :: thesis: verum