∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] (a b : α),
  Booleanisation.comp a < Booleanisation.comp b ↔
    Booleanisation.comp a ≤ Booleanisation.comp b ∧ ¬Booleanisation.comp b ≤ Booleanisation.comp a