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

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

hence
X is symmetric
; :: thesis: verum
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;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