set T = the complete Scott TopLattice;
take the complete Scott TopLattice ; :: thesis: ( the complete Scott TopLattice is order_consistent & the complete Scott TopLattice is complete )
thus ( the complete Scott TopLattice is order_consistent & the complete Scott TopLattice is complete ) by Th6; :: thesis: verum