let n, m be non zero Nat; :: thesis: FTSS2 (n,m) is symmetric
for x, y being Element of (FTSS2 (n,m)) st y in U_FT x holds
x in U_FT y

proof

let x, y be Element of (FTSS2 (n,m)); :: thesis: ( y in U_FT x implies x in U_FT y )
consider xu, xv being object such that
A1: xu in Seg n and
A2: xv in Seg m and
A3: x = [xu,xv] by ZFMISC_1:def 2;
reconsider i = xu, j = xv as Nat by A1, A2;
consider yu, yv being object such that
A4: yu in Seg n and
A5: yv in Seg m and
A6: y = [yu,yv] by ZFMISC_1:def 2;
reconsider i2 = yu, j2 = yv as Nat by A4, A5;
A7: FTSL1 m = RelStr(# (Seg m),(Nbdl1 m) #) by FINTOPO4:def 4;
then reconsider pj = j as Element of (FTSL1 m) by A2;
A8: FTSL1 n = RelStr(# (Seg n),(Nbdl1 n) #) by FINTOPO4:def 4;
then reconsider pi = i as Element of (FTSL1 n) by A1;
reconsider pj2 = j2 as Element of (FTSL1 m) by A7, A5;
reconsider pi2 = i2 as Element of (FTSL1 n) by A8, A4;
assume y in U_FT x ; :: thesis: x in U_FT y
then A9: y in [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:] by A3, Def4;

now :: thesis: ( ( y in [:{i},(Im ((Nbdl1 m),j)):] & x in [:{i2},(Im ((Nbdl1 m),j2)):] ) or ( y in [:(Im ((Nbdl1 n),i)),{j}:] & x in [:(Im ((Nbdl1 n),i2)),{j2}:] ) )

per cases ( y in [:{i},(Im ((Nbdl1 m),j)):] or y in [:(Im ((Nbdl1 n),i)),{j}:] ) by A9, XBOOLE_0:def 3;

case y in [:{i},(Im ((Nbdl1 m),j)):] ; :: thesis: x in [:{i2},(Im ((Nbdl1 m),j2)):]

then consider y1, y2 being object such that
A10: y1 in {i} and
A11: y2 in Class ((Nbdl1 m),j) and
A12: y = [y1,y2] by ZFMISC_1:def 2;
y1 = i by A10, TARSKI:def 1;
then A13: i in {i2} by A6, A10, A12, XTUPLE_0:1;
A14: FTSL1 m is symmetric by FINTOPO4:19;
pj2 in U_FT pj by A7, A6, A11, A12, XTUPLE_0:1;
then pj in U_FT pj2 by A14;
hence x in [:{i2},(Im ((Nbdl1 m),j2)):] by A3, A7, A13, ZFMISC_1:def 2; :: thesis: verum

end;

case y in [:(Im ((Nbdl1 n),i)),{j}:] ; :: thesis: x in [:(Im ((Nbdl1 n),i2)),{j2}:]

then consider y1, y2 being object such that
A15: y1 in Class ((Nbdl1 n),i) and
A16: y2 in {j} and
A17: y = [y1,y2] by ZFMISC_1:def 2;
y2 = j by A16, TARSKI:def 1;
then A18: j in {j2} by A6, A16, A17, XTUPLE_0:1;
A19: FTSL1 n is symmetric by FINTOPO4:19;
pi2 in U_FT pi by A8, A6, A15, A17, XTUPLE_0:1;
then pi in U_FT pi2 by A19;
hence x in [:(Im ((Nbdl1 n),i2)),{j2}:] by A3, A8, A18, ZFMISC_1:def 2; :: thesis: verum

end;

end;

end;

then x in [:{i2},(Im ((Nbdl1 m),j2)):] \/ [:(Im ((Nbdl1 n),i2)),{j2}:] by XBOOLE_0:def 3;
hence x in U_FT y by A6, Def4; :: thesis: verum

end;

hence FTSS2 (n,m) is symmetric ; :: thesis: verum