let n, m be non zero Element of NAT ; 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);
( y in U_FT x implies x in U_FT y )
consider xu,
xv being
set 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
Element of
NAT by A1, A2;
consider yu,
yv being
set 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
Element of
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
;
x in U_FT y
then A9:
y in [:{i},(Im (Nbdl1 m),j):] \/ [:(Im (Nbdl1 n),i),{j}:]
by A3, Def4;
now 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):]
;
x in [:{i2},(Im (Nbdl1 m),j2):]then consider y1,
y2 being
set 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, ZFMISC_1:33;
A14:
FTSL1 m is
symmetric
by FINTOPO4:19;
pj2 in U_FT pj
by A7, A6, A11, A12, ZFMISC_1:33;
then
pj in U_FT pj2
by A14, FIN_TOPO:def 15;
hence
x in [:{i2},(Im (Nbdl1 m),j2):]
by A3, A7, A13, ZFMISC_1:def 2;
verum end; case
y in [:(Im (Nbdl1 n),i),{j}:]
;
x in [:(Im (Nbdl1 n),i2),{j2}:]then consider y1,
y2 being
set 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, ZFMISC_1:33;
A19:
FTSL1 n is
symmetric
by FINTOPO4:19;
pi2 in U_FT pi
by A8, A6, A15, A17, ZFMISC_1:33;
then
pi in U_FT pi2
by A19, FIN_TOPO:def 15;
hence
x in [:(Im (Nbdl1 n),i2),{j2}:]
by A3, A8, A18, ZFMISC_1:def 2;
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 A6, Def4;
verum
end;
hence
FTSS2 n,m is symmetric
by FIN_TOPO:def 15; verum