let n, m be non zero Element of NAT ; :: thesis: FTSL2 n,m is filled
for x being Element of (FTSL2 n,m) holds x in U_FT x
proof
let x be
Element of
(FTSL2 n,m);
:: thesis: x in U_FT x
consider u,
y being
set such that A1:
(
u in Seg n &
y in Seg m &
x = [u,y] )
by ZFMISC_1:def 2;
reconsider i =
u,
j =
y as
Element of
NAT by A1;
A2:
FTSL1 m = RelStr(#
(Seg m),
(Nbdl1 m) #)
by FINTOPO4:def 4;
A3:
FTSL1 n = RelStr(#
(Seg n),
(Nbdl1 n) #)
by FINTOPO4:def 4;
then reconsider pi =
i as
Element of
(FTSL1 n) by A1;
reconsider pj =
j as
Element of
(FTSL1 m) by A1, A2;
FTSL1 n is
filled
by FINTOPO4:18;
then A4:
i in U_FT pi
by FIN_TOPO:def 4;
FTSL1 m is
filled
by FINTOPO4:18;
then
j in U_FT pj
by FIN_TOPO:def 4;
then
x in [:(Im (Nbdl1 n),i),(Im (Nbdl1 m),j):]
by A1, A2, A3, A4, ZFMISC_1:def 2;
hence
x in U_FT x
by A1, Def2;
:: thesis: verum
end;
hence
FTSL2 n,m is filled
by FIN_TOPO:def 4; :: thesis: verum