let n, m be non zero Element of NAT ; :: thesis: 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
let x,
y be
Element of
(FTSL2 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;
y in [:(Im (Nbdl1 n),i),(Im (Nbdl1 m),j):]
by A1, A2, Def2;
then consider y1,
y2 being
set such that A6:
(
y1 in Class (Nbdl1 n),
i &
y2 in Class (Nbdl1 m),
j &
y = [y1,y2] )
by ZFMISC_1:def 2;
A7:
pi2 in U_FT pi
by A4, A5, A6, ZFMISC_1:33;
FTSL1 n is
symmetric
by FINTOPO4:19;
then A8:
pi in U_FT pi2
by A7, FIN_TOPO:def 15;
A9:
j2 in U_FT pj
by A3, A5, A6, ZFMISC_1:33;
FTSL1 m is
symmetric
by FINTOPO4:19;
then
j in U_FT pj2
by A9, FIN_TOPO:def 15;
then
x in [:(Im (Nbdl1 n),i2),(Im (Nbdl1 m),j2):]
by A2, A3, A4, A8, ZFMISC_1:def 2;
hence
x in U_FT y
by A5, Def2;
:: thesis: verum
end;
hence
FTSL2 n,m is symmetric
by FIN_TOPO:def 15; :: thesis: verum