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