let FT be non empty RelStr ; :: thesis: for X being non empty SubSpace of FT st FT is filled holds
X is filled
let X be non empty SubSpace of FT; :: thesis: ( FT is filled implies X is filled )
assume A1: FT is filled ; :: thesis: X is filled
let x be Element of X; :: according to FIN_TOPO:def 4 :: thesis: x in U_FT x
the carrier of X c= the carrier of FT by Def2;
then reconsider x2 = x as Element of FT ;
A2: U_FT x = (U_FT x2) /\ ([#] X) by Def2;
x2 in U_FT x2 by A1;
hence x in U_FT x by A2, XBOOLE_0:def 4; :: thesis: verum