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 Th14
.= field O by Th14 ; :: thesis: verum