take the 0 -wff X -implied string of S ; :: thesis: the 0 -wff X -implied string of S is X -implied
thus the 0 -wff X -implied string of S is X -implied ; :: thesis: verum