set A = the empty array of a,X;
take the empty array of a,X ; :: thesis: ( the empty array of a,X is b -based & the empty array of a,X is natural-valued & the empty array of a,X is INT -valued & the empty array of a,X is real-valued & the empty array of a,X is complex-valued & the empty array of a,X is finite )
thus ( the empty array of a,X is b -based & the empty array of a,X is natural-valued & the empty array of a,X is INT -valued & the empty array of a,X is real-valued & the empty array of a,X is complex-valued & the empty array of a,X is finite ) ; :: thesis: verum