let
L
be
with_infima
Poset
;
:: thesis:
for
x
,
y
being
Element
of
(
L
opp
)
holds
(
~
x
)
"/\"
(
~
y
)
=
x
"\/"
y
let
x
,
y
be
Element
of
(
L
opp
)
;
:: thesis:
(
~
x
)
"/\"
(
~
y
)
=
x
"\/"
y
(
(
~
x
)
~
=
~
x
&
(
~
y
)
~
=
~
y
) ;
hence
(
~
x
)
"/\"
(
~
y
)
=
x
"\/"
y
by
Th21
;
:: thesis:
verum