:: deftheorem defines KModel MODELC_1:def 57 :
for S being non empty set
for S0 being Subset of S
for R being total Relation of S,S
for Prop being non empty Subset of (ModelSP S) holds KModel (R,S0,Prop) = KripkeStr(# S,S0,R,(Label_ Prop) #);