set R = the complete LATTICE;
set T = the correct strict Scott TopAugmentation of the complete LATTICE;
take the correct strict Scott TopAugmentation of the complete LATTICE ; :: thesis: ( the correct strict Scott TopAugmentation of the complete LATTICE is Scott & the correct strict Scott TopAugmentation of the complete LATTICE is complete & the correct strict Scott TopAugmentation of the complete LATTICE is strict )
thus ( the correct strict Scott TopAugmentation of the complete LATTICE is Scott & the correct strict Scott TopAugmentation of the complete LATTICE is complete & the correct strict Scott TopAugmentation of the complete LATTICE is strict ) ; :: thesis: verum