let
x
,
y
be
Element
of 1;
:: thesis:
(
op2
.
(
x
,
y
)
=
0
iff
x
=
y
)
A1
: (
x
=
{}
&
y
=
{}
)
by
CARD_1:49
,
TARSKI:def 1
;
hence
(
op2
.
(
x
,
y
)
=
0
implies
x
=
y
) ;
:: thesis:
(
x
=
y
implies
op2
.
(
x
,
y
)
=
0
)
thus
(
x
=
y
implies
op2
.
(
x
,
y
)
=
0
)
by
A1
,
Lm2
;
:: thesis:
verum