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 )

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

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 A8:
for A being Subset of FT holds A ^b = A ^f
; :: thesis: FT is symmetric
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

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;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 ^f or x in A ^b )
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;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

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

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