let
A
,
B
be non
empty
preBoolean
set
;
:: thesis:
for
a
,
b
being
Element
of
[:
A
,
B
:]
holds
a
/\
(
b
\/
a
)
=
a
let
a
,
b
be
Element
of
[:
A
,
B
:]
;
:: thesis:
a
/\
(
b
\/
a
)
=
a
thus
a
/\
(
b
\/
a
)
=
(
a
/\
b
)
\/
(
a
/\
a
)
by
Th5
.=
a
by
Th6
;
:: thesis:
verum