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

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

x in U_FT y

proof

hence
FTSS2 (n,m) is symmetric
; :: thesis: verum
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;

hence x in U_FT y by A6, Def4; :: thesis: verum

end;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}:] ) )end;

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

end;

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;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

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;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

hence x in U_FT y by A6, Def4; :: thesis: verum