let L be Lattice; :: thesis: <.L.) is prime
let p be Element of L; :: according to FILTER_0:def 6 :: thesis: for b₁ being Element of the carrier of L holds
( ( not p "\/" b₁ in <.L.) or p in <.L.) or b₁ in <.L.) ) & ( ( not p in <.L.) & not b₁ in <.L.) ) or p "\/" b₁ in <.L.) ) )
let q be Element of L; :: thesis: ( ( not p "\/" q in <.L.) or p in <.L.) or q in <.L.) ) & ( ( not p in <.L.) & not q in <.L.) ) or p "\/" q in <.L.) ) )
thus ( ( not p "\/" q in <.L.) or p in <.L.) or q in <.L.) ) & ( ( not p in <.L.) & not q in <.L.) ) or p "\/" q in <.L.) ) ) ; :: thesis: verum