let L1, L2 be non empty RelStr ; ( L1,L2 are_isomorphic implies L2,L1 are_isomorphic )
given f being Function of L1,L2 such that A1:
f is isomorphic
; WAYBEL_1:def 8 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
; verum