set L = the continuous complete LATTICE;

set T = the Scott TopAugmentation of the continuous complete LATTICE;

take the Scott TopAugmentation of the continuous complete LATTICE ; :: thesis: ( the Scott TopAugmentation of the continuous complete LATTICE is Scott & the Scott TopAugmentation of the continuous complete LATTICE is continuous & the Scott TopAugmentation of the continuous complete LATTICE is complete )

thus ( the Scott TopAugmentation of the continuous complete LATTICE is Scott & the Scott TopAugmentation of the continuous complete LATTICE is continuous & the Scott TopAugmentation of the continuous complete LATTICE is complete ) ; :: thesis: verum

set T = the Scott TopAugmentation of the continuous complete LATTICE;

take the Scott TopAugmentation of the continuous complete LATTICE ; :: thesis: ( the Scott TopAugmentation of the continuous complete LATTICE is Scott & the Scott TopAugmentation of the continuous complete LATTICE is continuous & the Scott TopAugmentation of the continuous complete LATTICE is complete )

thus ( the Scott TopAugmentation of the continuous complete LATTICE is Scott & the Scott TopAugmentation of the continuous complete LATTICE is continuous & the Scott TopAugmentation of the continuous complete LATTICE is complete ) ; :: thesis: verum