let f be non constant standard special_circular_sequence; (L~ f) ` = union { (Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `)))) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) }
A1:
the carrier of (TOP-REAL 2) = union { (cell ((GoB f),i,j)) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) }
by GOBRD11:7;
A2:
(L~ f) ` c= union { (Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `)))) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) }
proof
let x be
object ;
TARSKI:def 3 ( not x in (L~ f) ` or x in union { (Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `)))) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) } )
assume A3:
x in (L~ f) `
;
x in union { (Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `)))) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) }
then consider Y being
set such that A4:
(
x in Y &
Y in { (cell ((GoB f),i,j)) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) } )
by A1, TARSKI:def 4;
consider i,
j being
Nat such that A5:
Y = cell (
(GoB f),
i,
j)
and A6:
(
i <= len (GoB f) &
j <= width (GoB f) )
by A4;
reconsider Y0 =
Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `))) as
set ;
x in (cell ((GoB f),i,j)) /\ ((L~ f) `)
by A3, A4, A5, XBOOLE_0:def 4;
then A7:
x in Y0
by A6, Th2;
Y0 in { (Cl (Down ((Int (cell ((GoB f),i1,j1))),((L~ f) `)))) where i1, j1 is Nat : ( i1 <= len (GoB f) & j1 <= width (GoB f) ) }
by A6;
hence
x in union { (Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `)))) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) }
by A7, TARSKI:def 4;
verum
end;
union { (Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `)))) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) } c= (L~ f) `
proof
let x be
object ;
TARSKI:def 3 ( not x in union { (Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `)))) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) } or x in (L~ f) ` )
assume
x in union { (Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `)))) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) }
;
x in (L~ f) `
then consider Y being
set such that A8:
(
x in Y &
Y in { (Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `)))) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) } )
by TARSKI:def 4;
consider i,
j being
Nat such that A9:
Y = Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `)))
and
i <= len (GoB f)
and
j <= width (GoB f)
by A8;
Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `))) c= the
carrier of
((TOP-REAL 2) | ((L~ f) `))
;
then
Y c= (L~ f) `
by A9, Lm1;
hence
x in (L~ f) `
by A8;
verum
end;
hence
(L~ f) ` = union { (Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `)))) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) }
by A2, XBOOLE_0:def 10; verum