let f be non constant standard special_circular_sequence; :: thesis: (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 ; :: according to TARSKI:def 3 :: thesis: ( 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) ` ; :: thesis: 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; :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( 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) ) } ; :: thesis: 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; :: thesis: 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; :: thesis: verum