consider T being TopSpace;
take T | ({} T) ; :: thesis: ( T | ({} T) is strict & T | ({} T) is empty )
thus ( T | ({} T) is strict & T | ({} T) is empty ) ; :: thesis: verum