let L1, L2 be non empty RelStr ; :: thesis: ( L1,L2 are_isomorphic implies L2,L1 are_isomorphic )
given f being Function of L1,L2 such that A1: f is isomorphic ; :: according to WAYBEL_1:def 8 :: thesis: L2,L1 are_isomorphic
consider g being Function of L2,L1 such that
A2: g = f " and
A3: g is monotone by A1, WAYBEL_0:def 38;
f = g " by A1, A2, FUNCT_1:43;
then g is isomorphic by A1, A2, A3, WAYBEL_0:def 38;
hence L2,L1 are_isomorphic ; :: thesis: verum