set
A
= the non
empty
set
;
set
r
= the
Relation
of the non
empty
set
;
take
X
=
ARS
(# the non
empty
set
, the
Relation
of the non
empty
set
#);
:: thesis:
( not
X
is
empty
&
X
is
strict
)
thus
not
X
is
empty
;
:: thesis:
X
is
strict
thus
X
is
strict
;
:: thesis:
verum