let p, q be FinSequence; :: thesis: ( p is_a_prefix_of q implies ProperPrefixes p c= ProperPrefixes q )
assume A1: p is_a_prefix_of q ; :: thesis: ProperPrefixes p c= ProperPrefixes q
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ProperPrefixes p or x in ProperPrefixes q )
assume A2: x in ProperPrefixes p ; :: thesis: x in ProperPrefixes q
then reconsider r = x as FinSequence by Th10;
r is_a_proper_prefix_of p by A2, Th11;
then r is_a_proper_prefix_of q by A1, XBOOLE_1:58;
hence x in ProperPrefixes q by Th11; :: thesis: verum