theorem exists_in_the_understanding
theorem exists_in_the_understanding
(i : FoolUnderstandsTheWords)
(ii : WhateverIsUnderstoodExistsInTheUnderstanding)
(iii_bridge : ExistsInUnderstandingBridge)
: ExistsInTheUnderstanding