The Theory sets
 Parents
 basic_hol
 Children
 orders set_thms ℤ hol
 Constants
 IsSetRep ('a → BOOL) → BOOL \$SetComp ('a → BOOL) → 'a SET \$∈ 'a → 'a SET → BOOL {} 'a SET Universe 'a SET Insert 'a → 'a SET → 'a SET ~ 'a SET → 'a SET \$∪ 'a SET → 'a SET → 'a SET \$∩ 'a SET → 'a SET → 'a SET \$\ 'a SET → 'a SET → 'a SET \$⊖ 'a SET → 'a SET → 'a SET \$⊆ 'a SET → 'a SET → BOOL \$⊂ 'a SET → 'a SET → BOOL ⋃ 'a SET SET → 'a SET ⋂ 'a SET SET → 'a SET ℘ 'a SET → 'a SET SET
 Types
 '1 SET
 Fixity
 Binder: SetComp Left Infix 265: \ Right Infix 230: ⊆ ∈ ⊂ Right Infix 250: ⊖ Right Infix 260: ∪ Right Infix 270: ∩
 Definitions
 IsSetRep is_set_rep_def ⊢ IsSetRep = (λ x• T) SET set_def ⊢ ∃ f• TypeDefn IsSetRep f SetComp ∈ set_comp_def ⊢ ∀ x p a b • (x ∈ {v|p v} ⇔ p x) ∧ (a = b ⇔ (∀ x• x ∈ a ⇔ x ∈ b)) Empty Universe Insert insert_def ⊢ ∀ x y a • ¬ x ∈ {} ∧ x ∈ Universe ∧ (x ∈ Insert y a ⇔ x = y ∨ x ∈ a) ~ complement_def ⊢ ∀ x a• x ∈ ~ a ⇔ ¬ x ∈ a ∪ ∪_def ⊢ ∀ x a b• x ∈ a ∪ b ⇔ x ∈ a ∨ x ∈ b ∩ ∩_def ⊢ ∀ x a b• x ∈ a ∩ b ⇔ x ∈ a ∧ x ∈ b \ set_dif_def ⊢ ∀ x a b• x ∈ a \ b ⇔ x ∈ a ∧ ¬ x ∈ b ⊖ ⊖_def ⊢ ∀ x a b• x ∈ a ⊖ b ⇔ ¬ (x ∈ a ⇔ x ∈ b) ⊆ ⊆_def ⊢ ∀ a b• a ⊆ b ⇔ (∀ x• x ∈ a ⇒ x ∈ b) ⊂ ⊂_def ⊢ ∀ a b• a ⊂ b ⇔ a ⊆ b ∧ (∃ x• ¬ x ∈ a ∧ x ∈ b) ⋃ ⋃_def ⊢ ∀ x a• x ∈ ⋃ a ⇔ (∃ s• x ∈ s ∧ s ∈ a) ⋂ ⋂_def ⊢ ∀ x a• x ∈ ⋂ a ⇔ (∀ s• s ∈ a ⇒ x ∈ s) ℘ ℘_def ⊢ ∀ x a• x ∈ ℘ a ⇔ x ⊆ a
 Theorems
 sets_clauses ⊢ ∀ x y p q • (x ∈ {} ⇔ F) ∧ (x ∈ Universe ⇔ T) ∧ (x ∈ {v|q} ⇔ q) ∧ (x ∈ {v|p v} ⇔ p x) ∧ (x ∈ {v|v = y} ⇔ x = y) ∧ (x ∈ {y} ⇔ x = y) complement_clauses ⊢ (∀ x a• x ∈ ~ a ⇔ ¬ x ∈ a) ∧ ~ Universe = {} ∧ ~ {} = Universe ∪_clauses ⊢ ∀ a • a ∪ {} = a ∧ {} ∪ a = a ∧ a ∪ Universe = Universe ∧ Universe ∪ a = Universe ∧ a ∪ a = a ∩_clauses ⊢ ∀ a • a ∩ {} = {} ∧ {} ∩ a = {} ∧ a ∩ Universe = a ∧ Universe ∩ a = a ∧ a ∩ a = a set_dif_clauses ⊢ ∀ a • a \ {} = a ∧ {} \ a = {} ∧ a \ Universe = {} ∧ Universe \ a = ~ a ∧ a \ a = {} ⊖_clauses ⊢ ∀ a • a ⊖ {} = a ∧ {} ⊖ a = a ∧ a ⊖ Universe = ~ a ∧ Universe ⊖ a = ~ a ∧ a ⊖ a = {} ⊆_clauses ⊢ ∀ a• a ⊆ a ∧ {} ⊆ a ∧ a ⊆ Universe ⊂_clauses ⊢ ∀ a• ¬ a ⊂ a ∧ ¬ a ⊂ {} ∧ {} ⊂ Universe ⋃_clauses ⊢ ⋃ {} = {} ∧ ⋃ Universe = Universe ⋂_clauses ⊢ ⋂ {} = Universe ∧ ⋂ Universe = {} ℘_clauses ⊢ ∀ a • ℘ {} = {{}} ∧ ℘ Universe = Universe ∧ a ∈ ℘ a ∧ {} ∈ ℘ a ∅_clauses ⊢ ∀ x a • {x|F} = {} ∧ ¬ x ∈ {} ∧ {} ∪ a = a ∧ a ∪ {} = a ∧ {} ∩ a = {} ∧ a ∩ {} = {} ∧ a \ {} = a ∧ {} \ a = {} ∧ a ⊖ {} = a ∧ {} ⊖ a = a ∧ {} ⊆ a ∧ (a ⊆ {} ⇔ a = {}) ∧ ({} ⊂ a ⇔ ¬ a = {}) ∧ ¬ a ⊂ {} ∧ ¬ x ∈ ⋃ {} ∧ x ∈ ⋂ {} ∧ {} ∈ ℘ a ∧ ℘ {} = {{}} ∈_in_clauses ⊢ (∀ x y a • (x ∈ Universe ⇔ T) ∧ (x ∈ {} ⇔ F) ∧ (x ∈ Insert y a ⇔ x = y ∨ x ∈ a)) ∧ (∀ x a b • (x ∈ a ∪ b ⇔ x ∈ a ∨ x ∈ b) ∧ (x ∈ a ∩ b ⇔ x ∈ a ∧ x ∈ b) ∧ (x ∈ a \ b ⇔ x ∈ a ∧ ¬ x ∈ b) ∧ (x ∈ a ⊖ b ⇔ ¬ (x ∈ a ⇔ x ∈ b))) ∧ (∀ x a • (x ∈ ⋃ a ⇔ (∃ s• x ∈ s ∧ s ∈ a)) ∧ (x ∈ ⋂ a ⇔ (∀ s• s ∈ a ⇒ x ∈ s)) ∧ (∀ x a• x ∈ ℘ a ⇔ x ⊆ a)) sets_ext_clauses ⊢ ∀ a b • (a ⊂ b ⇔ (∀ x• x ∈ a ⇒ x ∈ b) ∧ (∃ x• ¬ x ∈ a ∧ x ∈ b)) ∧ (a ⊆ b ⇔ (∀ x• x ∈ a ⇒ x ∈ b)) ∧ (a = b ⇔ (∀ x• x ∈ a ⇔ x ∈ b))