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
A1: ( y = p & p is_a_proper_prefix_of <*x*> ) by Def4;
( len p < len <*x*> & len <*x*> = 1 & 1 = 0 + 1 ) by A1, Th24, FINSEQ_1:56;
then ( len p <= 0 & 0 <= len p ) by NAT_1:13;
then len p = 0 ;
then p = {} ;
hence y in {{} } by A1, 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 A2: ( y = {} & {} is_a_prefix_of <*x*> & {} <> <*x*> ) by TARSKI:def 1, XBOOLE_1:2;
then {} is_a_proper_prefix_of <*x*> by XBOOLE_0:def 8;
hence y in ProperPrefixes <*x*> by A2, Def4; :: thesis: verum