set RT = { [(root-tree t),s1] where s1 is Element of S : ex s being Element of S ex x being set st
( x in X . s & t = [x,s] & s <= s1 ) } ;
{ [(root-tree t),s1] where s1 is Element of S : ex s being Element of S ex x being set st
( x in X . s & t = [x,s] & s <= s1 ) } c= [:(TS (DTConOSA X)), the carrier of S:]
proof
let y be
object ;
TARSKI:def 3 ( not y in { [(root-tree t),s1] where s1 is Element of S : ex s being Element of S ex x being set st
( x in X . s & t = [x,s] & s <= s1 ) } or y in [:(TS (DTConOSA X)), the carrier of S:] )
assume
y in { [(root-tree t),s1] where s1 is Element of S : ex s being Element of S ex x being set st
( x in X . s & t = [x,s] & s <= s1 ) }
;
y in [:(TS (DTConOSA X)), the carrier of S:]
then consider s1 being
Element of
S such that A1:
y = [(root-tree t),s1]
and A2:
ex
s being
Element of
S ex
x being
set st
(
x in X . s &
t = [x,s] &
s <= s1 )
;
consider s being
Element of
S,
x being
set such that A3:
x in X . s
and A4:
t = [x,s]
and
s <= s1
by A2;
root-tree [x,s] is
Element of
TS (DTConOSA X)
by A3, Th10;
hence
y in [:(TS (DTConOSA X)), the carrier of S:]
by A1, A4, ZFMISC_1:def 2;
verum
end;
hence
{ [(root-tree t),s1] where s1 is Element of S : ex s being Element of S ex x being set st
( x in X . s & t = [x,s] & s <= s1 ) } is Subset of [:(TS (DTConOSA X)), the carrier of S:]
; verum