let n, m be non zero Nat; :: thesis: FTSL2 (n,m) is filled

for x being Element of (FTSL2 (n,m)) holds x in U_FT x

for x being Element of (FTSL2 (n,m)) holds x in U_FT x

proof

hence
FTSL2 (n,m) is filled
; :: thesis: verum
let x be Element of (FTSL2 (n,m)); :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum