set T = the TopSpace;
take the TopSpace | ({} the TopSpace) ; :: thesis: ( the TopSpace | ({} the TopSpace) is strict & the TopSpace | ({} the TopSpace) is empty )
thus ( the TopSpace | ({} the TopSpace) is strict & the TopSpace | ({} the TopSpace) is empty ) ; :: thesis: verum