set x = the Element of ProperPrefixes {};
assume A1: not ProperPrefixes {} = {} ; :: thesis: contradiction
then reconsider x = the Element of ProperPrefixes {} as FinSequence by Th10;
x is_a_proper_prefix_of {} by A1, Th11;
hence contradiction by XBOOLE_1:62; :: thesis: verum