let n, m be non zero Nat; :: thesis: FTSS2 (n,m) is filled
for x being Element of (FTSS2 (n,m)) holds x in U_FT x

proof

let x be Element of (FTSS2 (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: i in {i} by ZFMISC_1:31;
FTSL1 m is filled by FINTOPO4:18;
then j in U_FT pj ;
then x in [:{i},(Im ((Nbdl1 m),j)):] by A3, A4, A5, ZFMISC_1:def 2;
then x in [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{j}:] by XBOOLE_0:def 3;
hence x in U_FT x by A3, Def4; :: thesis: verum

end;

hence FTSS2 (n,m) is filled ; :: thesis: verum