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.) ) )
thus 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.) ) ) ; :: thesis: verum