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 A1: y in ProperPrefixes <*x*> ; :: thesis: y in {{} }
consider p being FinSequence such that
A2: y = p and
A3: p is_a_proper_prefix_of <*x*> by A1, Def4;
A4: len p < len <*x*> by A3, Th24;
A5: ( len <*x*> = 1 & 1 = 0 + 1 ) by FINSEQ_1:56;
A6: p = {} by A4, A5, NAT_1:13;
thus y in {{} } by A2, A6, 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 A7: y in {{} } ; :: thesis: y in ProperPrefixes <*x*>
A8: y = {} by A7, TARSKI:def 1;
A9: {} is_a_prefix_of <*x*> by XBOOLE_1:2;
A10: {} is_a_proper_prefix_of <*x*> by A9, XBOOLE_0:def 8;
thus y in ProperPrefixes <*x*> by A8, A10, Def4; :: thesis: verum