for E being non empty set
for F1, F2 being Subset of (E ^omega)
for TS1 being non empty transition-system over F1
for TS2 being non empty transition-system over F2 st the Tran of TS1 = the Tran of TS2 holds
==>.-relation TS1 = ==>.-relation TS2