let
M
be
MidSp
;
:: thesis:
for
p
,
q
being
Element
of
[:
the
carrier
of
M
, the
carrier
of
M
:]
st
p
~
=
q
~
holds
p
##
q
let
p
,
q
be
Element
of
[:
the
carrier
of
M
, the
carrier
of
M
:]
;
:: thesis:
(
p
~
=
q
~
implies
p
##
q
)
p
in
p
~
;
hence
(
p
~
=
q
~
implies
p
##
q
)
by
Th26
;
:: thesis:
verum