let FT be non empty RelStr ; :: thesis: for X being non empty SubSpace of FT st FT is symmetric holds
X is symmetric
let X be non empty SubSpace of FT; :: thesis: ( FT is symmetric implies X is symmetric )
assume A1: FT is symmetric ; :: thesis: X is symmetric
for x, y being Element of X st y in U_FT x holds
x in U_FT y

proof

let x, y be Element of X; :: thesis: ( y in U_FT x implies x in U_FT y )
assume A2: y in U_FT x ; :: thesis: x in U_FT y
the carrier of X c= the carrier of FT by Def2;
then reconsider x2 = x, y2 = y as Element of FT ;
A3: ( U_FT x = (U_FT x2) /\ ([#] X) & U_FT y = (U_FT y2) /\ ([#] X) ) by Def2;
( y2 in U_FT x2 implies x2 in U_FT y2 ) by A1;
hence x in U_FT y by A2, A3, XBOOLE_0:def 4; :: thesis: verum

end;

hence X is symmetric ; :: thesis: verum