let FT be non empty RelStr ; :: thesis: ( FT is symmetric iff for A being Subset of FT holds A ^b = A ^f )
thus ( FT is symmetric implies for A being Subset of FT holds A ^b = A ^f ) :: thesis: ( ( for A being Subset of FT holds A ^b = A ^f ) implies FT is symmetric )

proof

assume A1: FT is symmetric ; :: thesis: for A being Subset of FT holds A ^b = A ^f
let A be Subset of FT; :: thesis: A ^b = A ^f
thus A ^b c= A ^f :: according to XBOOLE_0:def 10 :: thesis: A ^f c= A ^b

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A ^b or x in A ^f )
assume A2: x in A ^b ; :: thesis: x in A ^f
then reconsider y = x as Element of FT ;
U_FT y meets A by A2, Th8;
then consider z being object such that
A3: z in (U_FT y) /\ A by XBOOLE_0:4;
reconsider z = z as Element of FT by A3;
z in U_FT y by A3, XBOOLE_0:def 4;
then A4: y in U_FT z by A1;
z in A by A3, XBOOLE_0:def 4;
hence x in A ^f by A4; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A ^f or x in A ^b )
assume A5: x in A ^f ; :: thesis: x in A ^b
then reconsider y = x as Element of FT ;
consider z being Element of FT such that
A6: z in A and
A7: y in U_FT z by A5, Th11;
z in U_FT y by A1, A7;
then U_FT y meets A by A6, XBOOLE_0:3;
hence x in A ^b ; :: thesis: verum

end;

assume A8: for A being Subset of FT holds A ^b = A ^f ; :: thesis: FT is symmetric
let x, y be Element of FT; :: according to FIN_TOPO:def 13 :: thesis: ( y in U_FT x implies x in U_FT y )
assume y in U_FT x ; :: thesis: x in U_FT y
then U_FT x meets {y} by ZFMISC_1:48;
then x in {y} ^b ;
then x in {y} ^f by A8;
then ex z being Element of FT st
( z in {y} & x in U_FT z ) by Th11;
hence x in U_FT y by TARSKI:def 1; :: thesis: verum