:: GOBRD11 semantic presentation

Lemma1: sqrt 2 > 0
by SQUARE_1:93;

theorem Th1: :: GOBRD11:1

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Point of b₁ st b₃ in b₂ & b₂ is connected holds
b₂ c= skl b₃

proof end;

theorem Th2: :: GOBRD11:2

for b₁ being non empty TopSpace
for b₂, b₃, b₄ being Subset of b₁ st b₄ is_a_component_of b₁ & b₂ c= b₄ & b₃ is connected & Cl b₂ meets Cl b₃ holds
b₃ c= b₄

proof end;

theorem Th3: :: GOBRD11:3

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is_a_component_of b₁ & b₃ is_a_component_of b₁ holds
b₂ \/ b₃ is a_union_of_components of b₁

proof end;

theorem Th4: :: GOBRD11:4

for b₁ being non empty TopSpace
for b₂, b₃, b₄ being Subset of b₁ holds Down (b₂ \/ b₃),b₄ = (Down b₂,b₄) \/ (Down b₃,b₄)

proof end;

theorem Th5: :: GOBRD11:5

for b₁ being non empty TopSpace
for b₂, b₃, b₄ being Subset of b₁ holds Down (b₂ /\ b₃),b₄ = (Down b₂,b₄) /\ (Down b₃,b₄)

proof end;

theorem Th6: :: GOBRD11:6

for b₁ being non constant standard special_circular_sequence holds (L~ b₁) ` <> {}

proof end;

registration

let c₁ be non constant standard special_circular_sequence;
cluster (L~ a₁) ` -> non empty ;
coherence by Th6;

end;

Lemma4: the carrier of (TOP-REAL 2) = REAL 2
by EUCLID:25;

theorem Th7: :: GOBRD11:7

for b₁ being non constant standard special_circular_sequence holds the carrier of (TOP-REAL 2) = union { (cell (GoB b₁),b₂,b₃) where B is Nat, B is Nat : ( b₂ <= len (GoB b₁) & b₃ <= width (GoB b₁) ) }

proof end;

Lemma5: for b₁ being Real holds { |[b₂,b₃]| where B is Real, B is Real : b₃ >= b₁ } is Subset of (TOP-REAL 2)

proof end;

Lemma6: for b₁ being Real holds { |[b₂,b₃]| where B is Real, B is Real : b₃ > b₁ } is Subset of (TOP-REAL 2)

proof end;

Lemma7: for b₁ being Real holds { |[b₂,b₃]| where B is Real, B is Real : b₃ <= b₁ } is Subset of (TOP-REAL 2)

proof end;

Lemma8: for b₁ being Real holds { |[b₂,b₃]| where B is Real, B is Real : b₃ < b₁ } is Subset of (TOP-REAL 2)

proof end;

Lemma9: for b₁ being Real holds { |[b₂,b₃]| where B is Real, B is Real : b₂ <= b₁ } is Subset of (TOP-REAL 2)

proof end;

Lemma10: for b₁ being Real holds { |[b₂,b₃]| where B is Real, B is Real : b₂ < b₁ } is Subset of (TOP-REAL 2)

proof end;

Lemma11: for b₁ being Real holds { |[b₂,b₃]| where B is Real, B is Real : b₂ >= b₁ } is Subset of (TOP-REAL 2)

proof end;

Lemma12: for b₁ being Real holds { |[b₂,b₃]| where B is Real, B is Real : b₂ > b₁ } is Subset of (TOP-REAL 2)

proof end;

theorem Th8: :: GOBRD11:8

for b₁ being Real
for b₂, b₃ being Subset of (TOP-REAL 2) st b₂ = { |[b₄,b₅]| where B is Real, B is Real : b₅ <= b₁ } & b₃ = { |[b₄,b₅]| where B is Real, B is Real : b₅ > b₁ } holds
b₂ = b₃ `

proof end;

theorem Th9: :: GOBRD11:9

for b₁ being Real
for b₂, b₃ being Subset of (TOP-REAL 2) st b₂ = { |[b₄,b₅]| where B is Real, B is Real : b₅ >= b₁ } & b₃ = { |[b₄,b₅]| where B is Real, B is Real : b₅ < b₁ } holds
b₂ = b₃ `

proof end;

theorem Th10: :: GOBRD11:10

for b₁ being Real
for b₂, b₃ being Subset of (TOP-REAL 2) st b₂ = { |[b₄,b₅]| where B is Real, B is Real : b₄ >= b₁ } & b₃ = { |[b₄,b₅]| where B is Real, B is Real : b₄ < b₁ } holds
b₂ = b₃ `

proof end;

theorem Th11: :: GOBRD11:11

for b₁ being Real
for b₂, b₃ being Subset of (TOP-REAL 2) st b₂ = { |[b₄,b₅]| where B is Real, B is Real : b₄ <= b₁ } & b₃ = { |[b₄,b₅]| where B is Real, B is Real : b₄ > b₁ } holds
b₂ = b₃ `

proof end;

theorem Th12: :: GOBRD11:12

for b₁ being Subset of (TOP-REAL 2)
for b₂ being Real st b₁ = { |[b₃,b₄]| where B is Real, B is Real : b₄ <= b₂ } holds
b₁ is closed

proof end;

theorem Th13: :: GOBRD11:13

for b₁ being Subset of (TOP-REAL 2)
for b₂ being Real st b₁ = { |[b₃,b₄]| where B is Real, B is Real : b₂ <= b₄ } holds
b₁ is closed

proof end;

theorem Th14: :: GOBRD11:14

for b₁ being Subset of (TOP-REAL 2)
for b₂ being Real st b₁ = { |[b₃,b₄]| where B is Real, B is Real : b₃ <= b₂ } holds
b₁ is closed

proof end;

theorem Th15: :: GOBRD11:15

for b₁ being Subset of (TOP-REAL 2)
for b₂ being Real st b₁ = { |[b₃,b₄]| where B is Real, B is Real : b₂ <= b₃ } holds
b₁ is closed

proof end;

theorem Th16: :: GOBRD11:16

for b₁ being Nat
for b₂ being Matrix of (TOP-REAL 2) holds h_strip b₂,b₁ is closed

proof end;

theorem Th17: :: GOBRD11:17

for b₁ being Nat
for b₂ being Matrix of (TOP-REAL 2) holds v_strip b₂,b₁ is closed

proof end;

theorem Th18: :: GOBRD11:18

for b₁ being V4 Matrix of (TOP-REAL 2) st b₁ is X_equal-in-line holds
v_strip b₁,0 = { |[b₂,b₃]| where B is Real, B is Real : b₂ <= (b₁ * 1,1) `1 }

proof end;

theorem Th19: :: GOBRD11:19

for b₁ being V4 Matrix of (TOP-REAL 2) st b₁ is X_equal-in-line holds
v_strip b₁,(len b₁) = { |[b₂,b₃]| where B is Real, B is Real : (b₁ * (len b₁),1) `1 <= b₂ }

proof end;

theorem Th20: :: GOBRD11:20

for b₁ being Nat
for b₂ being V4 Matrix of (TOP-REAL 2) st b₂ is X_equal-in-line & 1 <= b₁ & b₁ < len b₂ holds
v_strip b₂,b₁ = { |[b₃,b₄]| where B is Real, B is Real : ( (b₂ * b₁,1) `1 <= b₃ & b₃ <= (b₂ * (b₁ + 1),1) `1 ) }

proof end;

theorem Th21: :: GOBRD11:21

for b₁ being V4 Matrix of (TOP-REAL 2) st b₁ is Y_equal-in-column holds
h_strip b₁,0 = { |[b₂,b₃]| where B is Real, B is Real : b₃ <= (b₁ * 1,1) `2 }

proof end;

theorem Th22: :: GOBRD11:22

for b₁ being V4 Matrix of (TOP-REAL 2) st b₁ is Y_equal-in-column holds
h_strip b₁,(width b₁) = { |[b₂,b₃]| where B is Real, B is Real : (b₁ * 1,(width b₁)) `2 <= b₃ }

proof end;

theorem Th23: :: GOBRD11:23

for b₁ being Nat
for b₂ being V4 Matrix of (TOP-REAL 2) st b₂ is Y_equal-in-column & 1 <= b₁ & b₁ < width b₂ holds
h_strip b₂,b₁ = { |[b₃,b₄]| where B is Real, B is Real : ( (b₂ * 1,b₁) `2 <= b₄ & b₄ <= (b₂ * 1,(b₁ + 1)) `2 ) }

proof end;

theorem Th24: :: GOBRD11:24

for b₁ being V4 X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2) holds cell b₁,0,0 = { |[b₂,b₃]| where B is Real, B is Real : ( b₂ <= (b₁ * 1,1) `1 & b₃ <= (b₁ * 1,1) `2 ) }

proof end;

theorem Th25: :: GOBRD11:25

for b₁ being V4 X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2) holds cell b₁,0,(width b₁) = { |[b₂,b₃]| where B is Real, B is Real : ( b₂ <= (b₁ * 1,1) `1 & (b₁ * 1,(width b₁)) `2 <= b₃ ) }

proof end;

theorem Th26: :: GOBRD11:26

for b₁ being Nat
for b₂ being V4 X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2) st 1 <= b₁ & b₁ < width b₂ holds
cell b₂,0,b₁ = { |[b₃,b₄]| where B is Real, B is Real : ( b₃ <= (b₂ * 1,1) `1 & (b₂ * 1,b₁) `2 <= b₄ & b₄ <= (b₂ * 1,(b₁ + 1)) `2 ) }

proof end;

theorem Th27: :: GOBRD11:27

for b₁ being V4 X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2) holds cell b₁,(len b₁),0 = { |[b₂,b₃]| where B is Real, B is Real : ( (b₁ * (len b₁),1) `1 <= b₂ & b₃ <= (b₁ * 1,1) `2 ) }

proof end;

theorem Th28: :: GOBRD11:28

for b₁ being V4 X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2) holds cell b₁,(len b₁),(width b₁) = { |[b₂,b₃]| where B is Real, B is Real : ( (b₁ * (len b₁),1) `1 <= b₂ & (b₁ * 1,(width b₁)) `2 <= b₃ ) }

proof end;

theorem Th29: :: GOBRD11:29

for b₁ being Nat
for b₂ being V4 X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2) st 1 <= b₁ & b₁ < width b₂ holds
cell b₂,(len b₂),b₁ = { |[b₃,b₄]| where B is Real, B is Real : ( (b₂ * (len b₂),1) `1 <= b₃ & (b₂ * 1,b₁) `2 <= b₄ & b₄ <= (b₂ * 1,(b₁ + 1)) `2 ) }

proof end;

theorem Th30: :: GOBRD11:30

for b₁ being Nat
for b₂ being V4 X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2) st 1 <= b₁ & b₁ < len b₂ holds
cell b₂,b₁,0 = { |[b₃,b₄]| where B is Real, B is Real : ( (b₂ * b₁,1) `1 <= b₃ & b₃ <= (b₂ * (b₁ + 1),1) `1 & b₄ <= (b₂ * 1,1) `2 ) }

proof end;

theorem Th31: :: GOBRD11:31

for b₁ being Nat
for b₂ being V4 X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2) st 1 <= b₁ & b₁ < len b₂ holds
cell b₂,b₁,(width b₂) = { |[b₃,b₄]| where B is Real, B is Real : ( (b₂ * b₁,1) `1 <= b₃ & b₃ <= (b₂ * (b₁ + 1),1) `1 & (b₂ * 1,(width b₂)) `2 <= b₄ ) }

proof end;

theorem Th32: :: GOBRD11:32

for b₁, b₂ being Nat
for b₃ being V4 X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2) st 1 <= b₁ & b₁ < len b₃ & 1 <= b₂ & b₂ < width b₃ holds
cell b₃,b₁,b₂ = { |[b₄,b₅]| where B is Real, B is Real : ( (b₃ * b₁,1) `1 <= b₄ & b₄ <= (b₃ * (b₁ + 1),1) `1 & (b₃ * 1,b₂) `2 <= b₅ & b₅ <= (b₃ * 1,(b₂ + 1)) `2 ) }

proof end;

theorem Th33: :: GOBRD11:33

for b₁, b₂ being Nat
for b₃ being Matrix of (TOP-REAL 2) holds cell b₃,b₁,b₂ is closed

proof end;

theorem Th34: :: GOBRD11:34

for b₁ being V4 Matrix of (TOP-REAL 2) holds
( 1 <= len b₁ & 1 <= width b₁ )

proof end;

theorem Th35: :: GOBRD11:35

for b₁, b₂ being Nat
for b₃ being Go-board st b₁ <= len b₃ & b₂ <= width b₃ holds
cell b₃,b₁,b₂ = Cl (Int (cell b₃,b₁,b₂))

proof end;