let
x
be
Element
of
N
;
:: thesis:
x
is
Element
of
S
thus
x
is
Element
of
S
;
:: thesis:
verum