let
X
,
Y
,
Z
be
set
;
:: thesis:
(
X
in
Y
&
X
c=
Z
implies
meet
Y
c=
Z
)
assume
that
A1
:
X
in
Y
and
A2
:
X
c=
Z
;
:: thesis:
meet
Y
c=
Z
meet
Y
c=
X
by
A1
,
Th3
;
hence
meet
Y
c=
Z
by
A2
;
:: thesis:
verum