set T = the correct Scott TopAugmentation of R;
take the correct Scott TopAugmentation of R ; :: thesis: the correct Scott TopAugmentation of R is order_consistent
thus the correct Scott TopAugmentation of R is order_consistent by Th6; :: thesis: verum