let FT be non empty RelStr ; :: thesis: for X9 being SubSpace of FT

for A being Subset of X9 holds A is Subset of FT

let X9 be SubSpace of FT; :: thesis: for A being Subset of X9 holds A is Subset of FT

let A be Subset of X9; :: thesis: A is Subset of FT

the carrier of X9 c= the carrier of FT by Def2;

hence A is Subset of FT by XBOOLE_1:1; :: thesis: verum

for A being Subset of X9 holds A is Subset of FT

let X9 be SubSpace of FT; :: thesis: for A being Subset of X9 holds A is Subset of FT

let A be Subset of X9; :: thesis: A is Subset of FT

the carrier of X9 c= the carrier of FT by Def2;

hence A is Subset of FT by XBOOLE_1:1; :: thesis: verum