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