take {(0. X)} ; :: thesis: ( not {(0. X)} is empty & {(0. X)} is circled )
thus ( not {(0. X)} is empty & {(0. X)} is circled ) by Th26; :: thesis: verum