let R be non empty reflexive transitive antisymmetric up-complete RelStr ; :: thesis: ex T being TopAugmentation of R st T is Scott
set T = the Scott TopAugmentation of R;
take the Scott TopAugmentation of R ; :: thesis: the Scott TopAugmentation of R is Scott
thus the Scott TopAugmentation of R is Scott ; :: thesis: verum