Dotaz na tranzitivní uzávěr (4)

• b1am a b2 am+d nevyhovuje žádné klauzuli z .

• spor (amam+d Rs+ )

• (b) v existuje klauzule s atomy obsahujícími jen 

• Nechť b1b2 am+dam , kde ani bi am ani bi  am+d

• není obsaženo v  a d 0 je větší než libovolné c

• v b1b2+ c nebo b2 b1+ c v viz konstrukce )

• am+d am E(Rs) pro postačující s, ale Rs+ spor

• Tedy: Pro jakýkoliv výraz E vždy existuje s pro něž

• E(Rs) Rs+