take succ a ; :: according to EXCHSORT:def 1 :: thesis: ex b being Ordinal st proj1 {[a,x]} = (succ a) \ b
take a ; :: thesis: proj1 {[a,x]} = (succ a) \ a
thus dom {[a,x]} = {a} by FUNCT_5:12
.= (succ a) \ a by Th4 ; :: thesis: verum