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