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