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
A3: for x being set holds
( x in S1 iff ex q being FinSequence st
( x = q & q is_a_proper_prefix_of p ) ) and
A4: 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 );
A5: for x being set holds
( x in S1 iff S₁[x] ) by A3;
A6: for x being set holds
( x in S2 iff S₁[x] ) by A4;
thus S1 = S2 from XBOOLE_0:sch 2(A5, A6); :: thesis: verum