consider x being Element of ProperPrefixes {} ;
assume A1: not ProperPrefixes {} = {} ; :: thesis: contradiction
reconsider x = x as FinSequence by A1, Th35;
A2: x is_a_proper_prefix_of {} by A1, Th36;
thus contradiction by A2, XBOOLE_1:115; :: thesis: verum