set P = IdPrefSpace A;
set a = the Element of A;
B3: A = { the Element of A} by ZFMISC_1:132;
B2: A = the carrier of (IdPrefSpace A) by Def5;
ex a being Element of (IdPrefSpace A) st
( the PrefRel of (IdPrefSpace A) = [:{a},( the carrier of (IdPrefSpace A) \ {a}):] & the InternalRel of (IdPrefSpace A) = [:( the carrier of (IdPrefSpace A) \ {a}),( the carrier of (IdPrefSpace A) \ {a}):] )

proof

reconsider b = the Element of A as Element of (IdPrefSpace A) by Def5;
take b ; :: thesis: ( the PrefRel of (IdPrefSpace A) = [:{b},( the carrier of (IdPrefSpace A) \ {b}):] & the InternalRel of (IdPrefSpace A) = [:( the carrier of (IdPrefSpace A) \ {b}),( the carrier of (IdPrefSpace A) \ {b}):] )
B4: the carrier of (IdPrefSpace A) \ { the Element of A} = {} by XBOOLE_1:37, B2, B3;
s1: the PrefRel of (IdPrefSpace A) = {} (A,A) by Def5;
the InternalRel of (IdPrefSpace A) = {} (A,A) by Def5;
hence ( the PrefRel of (IdPrefSpace A) = [:{b},( the carrier of (IdPrefSpace A) \ {b}):] & the InternalRel of (IdPrefSpace A) = [:( the carrier of (IdPrefSpace A) \ {b}),( the carrier of (IdPrefSpace A) \ {b}):] ) by s1, B4; :: thesis: verum

end;

hence IdPrefSpace A is flat by B2, Def5; :: thesis: verum