:: deftheorem defines are_mutually_symmetric FINTOPO3:def 11 :
for S, T being non empty RelStr holds
( S,T are_mutually_symmetric iff ( the carrier of S = the carrier of T & ( for x being Element of S
for y being Element of T holds
( y in U_FT x iff x in U_FT y ) ) ) );