let x be set ; :: thesis: ProperPrefixes <*x*> = {{}}
thus ProperPrefixes <*x*> c= {{}} :: according to XBOOLE_0:def 10 :: thesis: {{}} is_a_prefix_of ProperPrefixes <*x*>

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in ProperPrefixes <*x*> or y in {{}} )
assume y in ProperPrefixes <*x*> ; :: thesis: y in {{}}
then consider p being FinSequence such that
A2: y = p and
A3: p is_a_proper_prefix_of <*x*> by Def4;
A4: len p < len <*x*> by A3, Th24;
( len <*x*> = 1 & 1 = 0 + 1 ) by FINSEQ_1:56;
then p = {} by A4, NAT_1:13;
hence y in {{}} by A2, TARSKI:def 1; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in {{}} or y in ProperPrefixes <*x*> )
assume y in {{}} ; :: thesis: y in ProperPrefixes <*x*>
then A8: y = {} by TARSKI:def 1;
{} is_a_prefix_of <*x*> by XBOOLE_1:2;
then {} is_a_proper_prefix_of <*x*> by XBOOLE_0:def 8;
hence y in ProperPrefixes <*x*> by A8, Def4; :: thesis: verum