:: deftheorem Def1 defines satisfiable GOEDCPUC:def 1 :
for Al being QC-alphabet
for PHI being Subset of (CQC-WFF Al) holds
( PHI is satisfiable iff ex A being non empty set ex J being interpretation of Al,A ex v being Element of Valuations_in (Al,A) st J,v |= PHI );