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

for x, y being Element of (FTSL2 (n,m)) st y in U_FT x holds

x in U_FT y

proof

hence
FTSL2 (n,m) is symmetric
; :: thesis: verum
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),(Nbdl1 m) #) by FINTOPO4:def 4;

then reconsider pj = j as Element of (FTSL1 m) by A3;

reconsider pj2 = j2 as Element of (FTSL1 m) by A8, A6;

assume y in U_FT x ; :: thesis: x in U_FT y

then y in [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] by A4, Def2;

then A9: ex y1, y2 being object st

( y1 in Class ((Nbdl1 n),i) & y2 in Class ((Nbdl1 m),j) & y = [y1,y2] ) by ZFMISC_1:def 2;

then j2 in U_FT pj by A8, A7, XTUPLE_0:1;

then A10: j in U_FT pj2 by A1;

A11: FTSL1 n = RelStr(# (Seg n),(Nbdl1 n) #) by FINTOPO4:def 4;

then reconsider pi = i as Element of (FTSL1 n) by A2;

A12: FTSL1 n is symmetric by FINTOPO4:19;

reconsider pi2 = i2 as Element of (FTSL1 n) by A11, A5;

pi2 in U_FT pi by A11, A7, A9, XTUPLE_0:1;

then pi in U_FT pi2 by A12;

then x in [:(Im ((Nbdl1 n),i2)),(Im ((Nbdl1 m),j2)):] by A4, A8, A11, A10, ZFMISC_1:def 2;

hence x in U_FT y by A7, Def2; :: thesis: verum

end;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),(Nbdl1 m) #) by FINTOPO4:def 4;

then reconsider pj = j as Element of (FTSL1 m) by A3;

reconsider pj2 = j2 as Element of (FTSL1 m) by A8, A6;

assume y in U_FT x ; :: thesis: x in U_FT y

then y in [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] by A4, Def2;

then A9: ex y1, y2 being object st

( y1 in Class ((Nbdl1 n),i) & y2 in Class ((Nbdl1 m),j) & y = [y1,y2] ) by ZFMISC_1:def 2;

then j2 in U_FT pj by A8, A7, XTUPLE_0:1;

then A10: j in U_FT pj2 by A1;

A11: FTSL1 n = RelStr(# (Seg n),(Nbdl1 n) #) by FINTOPO4:def 4;

then reconsider pi = i as Element of (FTSL1 n) by A2;

A12: FTSL1 n is symmetric by FINTOPO4:19;

reconsider pi2 = i2 as Element of (FTSL1 n) by A11, A5;

pi2 in U_FT pi by A11, A7, A9, XTUPLE_0:1;

then pi in U_FT pi2 by A12;

then x in [:(Im ((Nbdl1 n),i2)),(Im ((Nbdl1 m),j2)):] by A4, A8, A11, A10, ZFMISC_1:def 2;

hence x in U_FT y by A7, Def2; :: thesis: verum