let n, m be non zero Element of 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 )
assume A1:
y in U_FT x
;
:: thesis: x in U_FT y
consider xu,
xv being
set such that A2:
(
xu in Seg n &
xv in Seg m &
x = [xu,xv] )
by ZFMISC_1:def 2;
reconsider i =
xu,
j =
xv as
Element of
NAT by A2;
A3:
FTSL1 m = RelStr(#
(Seg m),
(Nbdl1 m) #)
by FINTOPO4:def 4;
A4:
FTSL1 n = RelStr(#
(Seg n),
(Nbdl1 n) #)
by FINTOPO4:def 4;
then reconsider pi =
i as
Element of
(FTSL1 n) by A2;
reconsider pj =
j as
Element of
(FTSL1 m) by A2, A3;
consider yu,
yv being
set such that A5:
(
yu in Seg n &
yv in Seg m &
y = [yu,yv] )
by ZFMISC_1:def 2;
reconsider i2 =
yu,
j2 =
yv as
Element of
NAT by A5;
reconsider pi2 =
i2 as
Element of
(FTSL1 n) by A4, A5;
reconsider pj2 =
j2 as
Element of
(FTSL1 m) by A3, A5;
A6:
y in [:{i},(Im (Nbdl1 m),j):] \/ [:(Im (Nbdl1 n),i),{j}:]
by A1, A2, Def4;
now per cases
( y in [:{i},(Im (Nbdl1 m),j):] or y in [:(Im (Nbdl1 n),i),{j}:] )
by A6, 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
set such that A7:
(
y1 in {i} &
y2 in Class (Nbdl1 m),
j &
y = [y1,y2] )
by ZFMISC_1:def 2;
A8:
y1 = i
by A7, TARSKI:def 1;
A9:
pj2 in U_FT pj
by A3, A5, A7, ZFMISC_1:33;
FTSL1 m is
symmetric
by FINTOPO4:19;
then A10:
pj in U_FT pj2
by A9, FIN_TOPO:def 15;
i in {i2}
by A5, A7, A8, ZFMISC_1:33;
hence
x in [:{i2},(Im (Nbdl1 m),j2):]
by A2, A3, A10, 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
set such that A11:
(
y1 in Class (Nbdl1 n),
i &
y2 in {j} &
y = [y1,y2] )
by ZFMISC_1:def 2;
A12:
y2 = j
by A11, TARSKI:def 1;
A13:
pi2 in U_FT pi
by A4, A5, A11, ZFMISC_1:33;
FTSL1 n is
symmetric
by FINTOPO4:19;
then A14:
pi in U_FT pi2
by A13, FIN_TOPO:def 15;
j in {j2}
by A5, A11, A12, ZFMISC_1:33;
hence
x in [:(Im (Nbdl1 n),i2),{j2}:]
by A2, A4, A14, ZFMISC_1:def 2;
:: thesis: verum 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 A5, Def4;
:: thesis: verum
end;
hence
FTSS2 n,m is symmetric
by FIN_TOPO:def 15; :: thesis: verum