let
x
be
set
;
:: thesis:
(
x
<>
{}
implies
x
tohilb
=
id
1 )
assume
x
<>
{}
;
:: thesis:
x
tohilb
=
id
1
then
reconsider
xx
=
x
as non
empty
set
;
xx
tohilb
=
id
1 ;
hence
x
tohilb
=
id
1 ;
:: thesis:
verum