let FT be non empty RelStr ; :: thesis: for X' being SubSpace of FT
for A being Subset of holds A is Subset of
let X' be SubSpace of FT; :: thesis: for A being Subset of holds A is Subset of
let A be Subset of ; :: thesis: A is Subset of
the carrier of X' c= the carrier of FT by Def2;
hence A is Subset of by XBOOLE_1:1; :: thesis: verum