th_PROP: THEORY
BEGIN

a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s,t,u,v,w,x,y,z: bool

A_0: PROPOSITION
     (a OR b OR c OR d OR e OR f OR g OR h OR i OR j OR k OR l OR m)
     IMPLIES
     (n AND o AND p AND q AND r AND s AND t AND u AND v AND w AND x AND y AND z)

END th_PROP