take
[#]
L
;
:: thesis:
[#]
L
is
prime
let
x
,
y
be
Element
of
L
;
:: according to
WAYBEL_7:def 2
:: thesis:
( not
x
"\/"
y
in
[#]
L
or
x
in
[#]
L
or
y
in
[#]
L
)
thus
( not
x
"\/"
y
in
[#]
L
or
x
in
[#]
L
or
y
in
[#]
L
) ;
:: thesis:
verum