take S ; :: according to SUBSTUT1:def 26 :: thesis: Sub_not S = Sub_not S
thus Sub_not S = Sub_not S ; :: thesis: verum