src/ZF/AC/first.thy

Numerous small improvements by KG and LCP

(*  Title: 	ZF/AC/first.thy
    ID:         $Id$
    Author: 	Krzysztof Gr`abczewski

Theory helpful in proofs using first element of a well ordered set
*)

first = Order +

consts

  first                   :: "[i, i, i] => o"

defs

  first_def                "first(u, X, R) 
			    == u:X & (ALL v:X. v~=u --> <u,v> : R)"

end