let S1, S2 be set ; :: thesis: ( ( for x being set holds
( x in S1 iff ex q being FinSequence st
( x = q & q is_a_proper_prefix_of p ) ) ) & ( for x being set holds
( x in S2 iff ex q being FinSequence st
( x = q & q is_a_proper_prefix_of p ) ) ) implies S1 = S2 )
assume that
A10: for x being set holds
( x in S1 iff ex q being FinSequence st
( x = q & q is_a_proper_prefix_of p ) ) and
A11: for x being set holds
( x in S2 iff ex q being FinSequence st
( x = q & q is_a_proper_prefix_of p ) ) ; :: thesis: S1 = S2
defpred S₁[ set ] means ex q being FinSequence st
( $1 = q & q is_a_proper_prefix_of p );
A12: for x being set holds
( x in S1 iff S₁[x] ) by A10;
A13: for x being set holds
( x in S2 iff S₁[x] ) by A11;
thus S1 = S2 from XBOOLE_0:sch 2(A12, A13); :: thesis: verum