Although h53::noneabove.4 |- ( th <-> ( ph \/ ps \/ ch ) ) is not a correct interpretation of "[Exactly] One of the above", it is rather "[At least] One of the

Although h53::noneabove.4 |- ( th <-> ( ph \/ ps \/ ch ) ) is not a correct interpretation of "[Exactly] One of the above", it is rather "[At least] One of the above", it doesn't matter because 'th' is not true anyway.