consider
b
being
Element
of
L
such that
A1
:
B
=
(
StoneH
L
)
.
b
by
Th13
;
consider
a
being
Element
of
L
such that
A2
:
A
=
(
StoneH
L
)
.
a
by
Th13
;
A
\/
B
=
(
StoneH
L
)
.
(
a
"\/"
b
)
by
A2
,
A1
,
Th14
;
hence
A
\/
B
is
Element
of
StoneS
L
by
Th13
;
:: thesis:
verum