Section AND.

  Variable p q : Prop.


  Definition AND := forall r : Prop, (p -> q -> r) -> r.


        Variable h1 : p.
        Variable h2 : q.

                Theorem and : AND.
                Proof fun (r : Prop) (h : p -> q -> r) => h h1 h2.

End AND.

Notation "A /\ B" := (AND A B) : type_scope.


Section Tarski.


  Variable A : Type.
  Variable R : A -> A -> Prop.
  Variable Rtrans : forall x y z : A, R x y -> R y z -> R x z.
  Variable F : (A -> Prop) -> A.
  Variable Upperb : forall (P : A -> Prop) (x : A), P x -> R x (F P).
  Variable
    Least :
      forall (P : A -> Prop) (x : A),
      (forall y : A, P y -> R y x) -> R (F P) x.
  Variable f : A -> A.
  Variable Incr : forall x y : A, R x y -> R (f x) (f y).


  Definition P0 (x : A) := R x (f x).
  Definition x0 := F P0.


Section lemme1.

        Variable x : A.
        Variable h1 : R x (f x).
        Theorem lemme1 : R x (f x0).
        Proof Rtrans x (f x) (f x0) h1 (Incr x x0 (Upperb P0 x h1)).

End lemme1.

Lemma fact1 : R x0 (f x0).
Proof Least P0 (f x0) lemme1.

Lemma fact2 : R (f x0) x0.
Proof Upperb P0 (f x0) (Incr x0 (f x0) fact1).

Theorem Tarski : R x0 (f x0) /\ R (f x0) x0.
Proof and (R x0 (f x0)) (R (f x0) x0) fact1 fact2.

End Tarski.


Section Knaster.

  Variable U : Type.

  Definition set := U -> Prop.
  Definition Subset (x y : set) := forall u : U, x u -> y u.
  Definition Equal (x y : set) := Subset x y /\ Subset y x.
  Definition Class := set -> Prop.
  Definition Map := set -> set.
  Variable Phi : Map.
  Variable Incr : forall x y : set, Subset x y -> Subset (Phi x) (Phi y).

  Definition Over (C : Class) (x : set) := forall y : set, C y -> Subset y x.
  Definition Union (C : Class) (u : U) := forall x : set, Over C x -> x u.

  Definition Subset_trans (x y z : set) (h1 : Subset x y)
    (h2 : Subset y z) (u : U) (h3 : x u) := h2 u (h1 u h3).
  Definition Union_upperb (C : Class) (x : set) (h1 : C x)
    (u : U) (h2 : x u) (y : set) (h3 : Over C y) :=
    h3 x h1 u h2.
  Definition Union_least (C : Class) (x : set)
    (h1 : forall y : set, C y -> Subset y x) (u : U)
    (h2 : Union C u) := h2 x h1.

  Definition Stable (x : set) := Subset x (Phi x).
  Definition S := Union Stable.

Lemma Knaster : Equal S (Phi S).
Proof Tarski set Subset Subset_trans Union Union_upperb Union_least Phi Incr.

End Knaster.