let
A
,
B
,
X
,
Y
be
set
;
:: thesis:
(
A
c=
X
&
B
c=
Y
&
X
misses
Y
implies
A
misses
B
)
assume
that
A1
:
A
c=
X
and
A2
:
B
c=
Y
and
A3
:
X
misses
Y
;
:: thesis:
A
misses
B
A
misses
Y
by
A1
,
A3
,
Th63
;
hence
A
misses
B
by
A2
,
Th63
;
:: thesis:
verum