take
S
=
2-sorted
(# 1,
{
0
,1
}
#);
:: thesis:
not
S
is
trivial'
(
0
in
{
0
,1
}
& 1
in
{
0
,1
}
)
by
TARSKI:def 2
;
hence
not
S
is
trivial'
by
ZFMISC_1:def 10
;
:: thesis:
verum