let FT be non empty RelStr ; :: thesis: for X being non empty SubSpace of FT st FT is reflexive holds
X is reflexive
let X be non empty SubSpace of FT; :: thesis: ( FT is reflexive implies X is reflexive )
assume A1: FT is reflexive ; :: thesis: X is reflexive
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 by TARSKI:def 3;
A2: U_FT x = (U_FT x2) /\ ([#] X) by Def2;
x2 in U_FT x2 by A1, FIN_TOPO:def 4;
hence x in U_FT x by A2, XBOOLE_0:def 4; :: thesis: verum