consider
k
being
Element
of
F
such that
A2
:
a
_|_
by
A1
,
Def1
;
take
k
;
:: thesis:
for
l
being
Element
of
F
st
a
_|_
holds
k
=
l
let
l
be
Element
of
F
;
:: thesis:
(
a
_|_
implies
k
=
l
)
assume
a
_|_
;
:: thesis:
k
=
l
hence
k
=
l
by
A1
,
A2
,
Th8
;
:: thesis:
verum