:: deftheorem defines symmetric FIN_TOPO:def 13 :
for IT being non empty RelStr holds
( IT is symmetric iff for x, y being Element of IT st y in U_FT x holds
x in U_FT y );