set P = <* the Element of A*>;
take <* the Element of A*> ; :: thesis: ( not <* the Element of A*> is empty & <* the Element of A*> is A,R -correct )
thus not <* the Element of A*> is empty ; :: thesis: <* the Element of A*> is A,R -correct
thus <* the Element of A*> is A,R -correct by Th40; :: thesis: verum