reconsider
xx
=
x
as
set
by
TARSKI:1
;
not
xx
in
xx
;
hence
( (
x
in
y
implies
a
is
object
) & (
x
=
y
implies
b
is
object
) & ( not
x
in
y
& not
x
=
y
implies
c
is
object
) & ( for
b
_{1}
being
object
st
x
in
y
&
x
=
y
holds
(
b
_{1}
=
a
iff
b
_{1}
=
b
) ) ) ;
:: thesis:
verum