let X be set ; :: thesis: for O being Order of X holds field O = X
let O be Order of X; :: thesis: field O = X
thus X = X \/ X
.= (dom O) \/ X by Th99
.= field O by Th99 ; :: thesis: verum