:: deftheorem defines Example_Formula_of GOEDCPUC:def 5 :
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds Example_Formula_of (p,x) = ('not' (Ex (((FCEx Al) -Cast x),((FCEx Al) -Cast p)))) 'or' (((FCEx Al) -Cast p) . (((FCEx Al) -Cast x),(Example_of (p,x))));