let
s
be
set
;
:: thesis:
(
s
is
Element
of
ARS_01
iff (
s
=
0
or
s
=
1 ) )
the
carrier
of
ARS_01
=
{
0
,1
}
by
Def18
;
hence
(
s
is
Element
of
ARS_01
iff (
s
=
0
or
s
=
1 ) )
by
TARSKI:def 2
;
:: thesis:
verum