defpred S₁[ object ] means for p being FinSequence of NAT st $1 = p holds
for q being FinSequence of NAT st q in T holds
not p is_a_proper_prefix_of q;
consider X being set such that
A1: for x being object holds
( x in X iff ( x in T & S₁[x] ) ) from XBOOLE_0:sch 1();
X c= T by A1;
then reconsider X = X as Subset of T ;
take X ; :: thesis: for p being FinSequence of NAT holds
( p in X iff ( p in T & ( for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) ) ) )
let p be FinSequence of NAT ; :: thesis: ( p in X iff ( p in T & ( for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) ) ) )
thus ( p in X implies ( p in T & ( for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) ) ) ) by A1; :: thesis: ( p in T & ( for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) ) implies p in X )
assume that
A2: p in T and
A3: for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) ; :: thesis: p in X
for r being FinSequence of NAT st p = r holds
for q being FinSequence of NAT st q in T holds
not r is_a_proper_prefix_of q by A3;
hence p in X by A1, A2; :: thesis: verum