take [#] L ; :: thesis: [#] L is prime
let x, y be Element of L; :: according to WAYBEL_7:def 1 :: 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