let n, m be non zero Nat; 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
proof
A1:
FTSL1 m is
symmetric
by FINTOPO4:19;
let x,
y be
Element of
(FTSL2 (n,m));
( 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
;
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;
verum
end;
hence
FTSL2 (n,m) is symmetric
; verum