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 object ; :: 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 and
A2: p is_a_proper_prefix_of <*x*> by Def2;
A3: len p < len <*x*> by A2, Th5;
( len <*x*> = 1 & 1 = 0 + 1 ) by FINSEQ_1:39;
then p = {} by A3, NAT_1:13;
hence y in {{}} by A1, TARSKI:def 1; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in {{}} or y in ProperPrefixes <*x*> )
assume y in {{}} ; :: thesis: y in ProperPrefixes <*x*>
then A4: y = {} by TARSKI:def 1;
{} is_a_prefix_of <*x*> ;
then {} is_a_proper_prefix_of <*x*> ;
hence y in ProperPrefixes <*x*> by A4, Def2; :: thesis: verum