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

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