let n, m be non zero Nat; :: thesis: FTSL2 (n,m) is symmetric
for x, y being Element of (FTSL2 (n,m)) st y in U_FT x holds
x in U_FT y
proof
A1: FTSL1 m is symmetric by FINTOPO4:19;
let x, y be Element of (FTSL2 (n,m)); :: thesis: ( y in U_FT x implies x in U_FT y )
consider xu, xv being object such that
A2: xu in Seg n and
A3: xv in Seg m and
A4: x = [xu,xv] by ZFMISC_1:def 2;
reconsider i = xu, j = xv as Nat by A2, A3;
consider yu, yv being object such that
A5: yu in Seg n and
A6: yv in Seg m and
A7: y = [yu,yv] by ZFMISC_1:def 2;
reconsider i2 = yu, j2 = yv as Nat by A5, A6;
A8: FTSL1 m = RelStr(# (Seg m),() #) by FINTOPO4:def 4;
then reconsider pj = j as Element of () by A3;
reconsider pj2 = j2 as Element of () by A8, A6;
assume y in U_FT x ; :: thesis: x in U_FT y
then y in [:(Im ((),i)),(Im ((),j)):] by ;
then A9: ex y1, y2 being object st
( y1 in Class ((),i) & y2 in Class ((),j) & y = [y1,y2] ) by ZFMISC_1:def 2;
then j2 in U_FT pj by ;
then A10: j in U_FT pj2 by A1;
A11: FTSL1 n = RelStr(# (Seg n),() #) by FINTOPO4:def 4;
then reconsider pi = i as Element of () by A2;
A12: FTSL1 n is symmetric by FINTOPO4:19;
reconsider pi2 = i2 as Element of () by ;
pi2 in U_FT pi by ;
then pi in U_FT pi2 by A12;
then x in [:(Im ((),i2)),(Im ((),j2)):] by ;
hence x in U_FT y by ; :: thesis: verum
end;
hence FTSL2 (n,m) is symmetric ; :: thesis: verum