set R = the empty RelStr ;
take the empty RelStr ; :: thesis: ( the empty RelStr is non empty connected Poset or the empty RelStr is empty )
thus ( the empty RelStr is non empty connected Poset or the empty RelStr is empty ) ; :: thesis: verum