take 0. S ; :: thesis: 0. S is zero
thus 0. S = 0. S ; :: according to STRUCT_0:def 12 :: thesis: verum