let n, m be non zero Nat; 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));
x in U_FT x
consider u,
y being
object such that A1:
u in Seg n
and A2:
y in Seg m
and A3:
x = [u,y]
by ZFMISC_1:def 2;
reconsider i =
u,
j =
y as
Nat by A1, A2;
A4:
FTSL1 m = RelStr(#
(Seg m),
(Nbdl1 m) #)
by FINTOPO4:def 4;
then reconsider pj =
j as
Element of
(FTSL1 m) by A2;
A5:
FTSL1 n = RelStr(#
(Seg n),
(Nbdl1 n) #)
by FINTOPO4:def 4;
then reconsider pi =
i as
Element of
(FTSL1 n) by A1;
FTSL1 m is
filled
by FINTOPO4:18;
then A6:
j in U_FT pj
;
FTSL1 n is
filled
by FINTOPO4:18;
then
i in U_FT pi
;
then
x in [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):]
by A3, A4, A5, A6, ZFMISC_1:def 2;
hence
x in U_FT x
by A3, Def2;
verum
end;
hence
FTSL2 (n,m) is filled
; verum