Vecerajúci filozofi 3
Dôkaz odvodenej vlastnosti pre user (stable ?u.e):
u.t unless u.h in user /* (udn1) */
u.h unless false in user /* def. stable pre (udn2) */
u.t ? u.h unless false in user /* tranzitivita pre unless */
u.t ? u.h ? ?u.e /* práve jedna z hodnôt */
?u.e unless false in user ? stable ?u.e in user
naša snaha: špecifikovat vlastnosti os; teda všetko bude pre os, ak nebude výslovne uvedené inak