let
a
,
b
be
Element
of
Trivial-multLoopStr
;
:: thesis:
a
=
b
thus
a
=
{}
by
TARSKI:def 1
.=
b
by
TARSKI:def 1
;
:: thesis:
verum