(
Tr:(Term
Prop), tr:Term, L:(TermProp). RepsTruth(L; Tr; tr))
S:Term. (t:Term. S 
= t) 
L(SUBX(tr; S))) & RespectsNot(Tr; L) & ReflectsProp(Tr; tr; Tr)
is mentioned by
| Thm* (Tr:(TermProp), tr:Term, L:(TermProp). RepsTruth(L; Tr; tr)) | [Tarski] |