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