ModelSP the Worlds of (KModel R,S0,Prop) c= Funcs the Worlds of (KModel R,S0,Prop),BOOLEAN ;
hence ModelSP the Worlds of (KModel R,S0,Prop) is non empty Subset of (Funcs the Worlds of (KModel R,S0,Prop),BOOLEAN ) ; :: thesis: verum