set S = the non empty non void 1-1-connectives bool-correct BoolSignature ;
take the non empty non void 1-1-connectives bool-correct BoolSignature ; :: thesis: ( the non empty non void 1-1-connectives bool-correct BoolSignature is 1-1-connectives & not the non empty non void 1-1-connectives bool-correct BoolSignature is empty & not the non empty non void 1-1-connectives bool-correct BoolSignature is void )
thus ( the non empty non void 1-1-connectives bool-correct BoolSignature is 1-1-connectives & not the non empty non void 1-1-connectives bool-correct BoolSignature is empty & not the non empty non void 1-1-connectives bool-correct BoolSignature is void ) ; :: thesis: verum