let D be non empty set ; :: thesis: for B, A being set st B is D -prefix & A c= B holds
A is D -prefix
let B, A be set ; :: thesis: ( B is D -prefix & A c= B implies A is D -prefix )
set f = D -concatenation ;
assume ( B is D -prefix & A c= B ) ; :: thesis: A is D -prefix
then ( B is D -concatenation -unambiguous & A c= B ) by DefPrefix;
then A is D -concatenation -unambiguous by Lm13;
hence A is D -prefix by DefPrefix; :: thesis: verum