:: YELLOW17 semantic presentation

theorem Th1: :: YELLOW17:1
for b1 being Function
for b2, b3 being set
for b4 being Subset of (b1 . b2) st (proj b1,b2) " {b3} meets (proj b1,b2) " b4 holds
b3 in b4
proof end;

theorem Th2: :: YELLOW17:2
for b1, b2 being Function
for b3, b4 being set st b4 in b1 . b3 & b2 in product b1 holds
b2 +* b3,b4 in product b1
proof end;

theorem Th3: :: YELLOW17:3
for b1 being Function
for b2 being set st b2 in dom b1 & product b1 <> {} holds
rng (proj b1,b2) = b1 . b2
proof end;

theorem Th4: :: YELLOW17:4
for b1 being Function
for b2 being set st b2 in dom b1 holds
(proj b1,b2) " (b1 . b2) = product b1
proof end;

theorem Th5: :: YELLOW17:5
for b1, b2 being Function
for b3, b4 being set st b4 in b1 . b3 & b3 in dom b1 & b2 in product b1 holds
b2 +* b3,b4 in (proj b1,b3) " {b4}
proof end;

Lemma6: for b1, b2 being Function
for b3, b4, b5 being set
for b6 being Subset of (b1 . b4) st b3 <> b4 & b2 in product b1 & b2 +* b3,b5 in (proj b1,b4) " b6 holds
b2 in (proj b1,b4) " b6
proof end;

theorem Th6: :: YELLOW17:6
for b1, b2 being Function
for b3, b4, b5 being set
for b6 being Subset of (b1 . b4) st b5 in b1 . b3 & b3 in dom b1 & b2 in product b1 & b3 <> b4 holds
( b2 in (proj b1,b4) " b6 iff b2 +* b3,b5 in (proj b1,b4) " b6 )
proof end;

theorem Th7: :: YELLOW17:7
for b1 being Function
for b2, b3, b4 being set
for b5 being Subset of (b1 . b3) st product b1 <> {} & b4 in b1 . b2 & b2 in dom b1 & b3 in dom b1 & b5 <> b1 . b3 holds
( (proj b1,b2) " {b4} c= (proj b1,b3) " b5 iff ( b2 = b3 & b4 in b5 ) )
proof end;

scheme :: YELLOW17:sch 1
s1{ F1() -> non empty set , F2() -> non-Empty TopSpace-yielding ManySortedSet of F1(), P1[ set , set ] } :
ex b1 being Element of (product F2()) st
for b2 being Element of F1() holds P1[b1 . b2,b2]
provided
E9: for b1 being Element of F1() ex b2 being Element of (F2() . b1) st P1[b2,b1]
proof end;

theorem Th8: :: YELLOW17:8
for b1 being non empty set
for b2 being non-Empty TopSpace-yielding ManySortedSet of b1
for b3 being Element of b1
for b4 being Element of (product b2) holds (proj b2,b3) . b4 = b4 . b3
proof end;

theorem Th9: :: YELLOW17:9
for b1 being non empty set
for b2 being non-Empty TopSpace-yielding ManySortedSet of b1
for b3 being Element of b1
for b4 being Element of (b2 . b3)
for b5 being Subset of (b2 . b3) st (proj b2,b3) " {b4} meets (proj b2,b3) " b5 holds
b4 in b5
proof end;

theorem Th10: :: YELLOW17:10
for b1 being non empty set
for b2 being non-Empty TopSpace-yielding ManySortedSet of b1
for b3 being Element of b1 holds (proj b2,b3) " ([#] (b2 . b3)) = [#] (product b2)
proof end;

theorem Th11: :: YELLOW17:11
for b1 being non empty set
for b2 being non-Empty TopSpace-yielding ManySortedSet of b1
for b3 being Element of b1
for b4 being Element of (b2 . b3)
for b5 being Element of (product b2) holds b5 +* b3,b4 in (proj b2,b3) " {b4}
proof end;

theorem Th12: :: YELLOW17:12
for b1 being non empty set
for b2 being non-Empty TopSpace-yielding ManySortedSet of b1
for b3, b4 being Element of b1
for b5 being Element of (b2 . b3)
for b6 being Subset of (b2 . b4) st b6 <> [#] (b2 . b4) holds
( (proj b2,b3) " {b5} c= (proj b2,b4) " b6 iff ( b3 = b4 & b5 in b6 ) )
proof end;

theorem Th13: :: YELLOW17:13
for b1 being non empty set
for b2 being non-Empty TopSpace-yielding ManySortedSet of b1
for b3, b4 being Element of b1
for b5 being Element of (b2 . b3)
for b6 being Subset of (b2 . b4)
for b7 being Element of (product b2) st b3 <> b4 holds
( b7 in (proj b2,b4) " b6 iff b7 +* b3,b5 in (proj b2,b4) " b6 )
proof end;

theorem Th14: :: YELLOW17:14
canceled;

theorem Th15: :: YELLOW17:15
for b1 being non empty TopStruct holds
( b1 is compact iff for b2 being Subset-Family of b1 st b2 is open & [#] b1 c= union b2 holds
ex b3 being Subset-Family of b1 st
( b3 c= b2 & [#] b1 c= union b3 & b3 is finite ) )
proof end;

theorem Th16: :: YELLOW17:16
for b1 being non empty TopSpace
for b2 being prebasis of b1 holds
( b1 is compact iff for b3 being Subset of b2 st [#] b1 c= union b3 holds
ex b4 being finite Subset of b3 st [#] b1 c= union b4 )
proof end;

theorem Th17: :: YELLOW17:17
for b1 being non empty set
for b2 being non-Empty TopSpace-yielding ManySortedSet of b1
for b3 being set st b3 in product_prebasis b2 holds
ex b4 being Element of b1ex b5 being Subset of (b2 . b4) st
( b5 is open & (proj b2,b4) " b5 = b3 )
proof end;

theorem Th18: :: YELLOW17:18
for b1 being non empty set
for b2 being non-Empty TopSpace-yielding ManySortedSet of b1
for b3 being Element of b1
for b4 being Element of (b2 . b3)
for b5 being set st b5 in product_prebasis b2 & (proj b2,b3) " {b4} c= b5 & not b5 = [#] (product b2) holds
ex b6 being Subset of (b2 . b3) st
( b6 <> [#] (b2 . b3) & b4 in b6 & b6 is open & b5 = (proj b2,b3) " b6 )
proof end;

theorem Th19: :: YELLOW17:19
for b1 being non empty set
for b2 being non-Empty TopSpace-yielding ManySortedSet of b1
for b3 being Element of b1
for b4 being non empty Subset-Family of (b2 . b3) st [#] (b2 . b3) c= union b4 holds
[#] (product b2) c= union { ((proj b2,b3) " b5) where B is Element of b4 : verum }
proof end;

theorem Th20: :: YELLOW17:20
for b1 being non empty set
for b2 being non-Empty TopSpace-yielding ManySortedSet of b1
for b3 being Element of b1
for b4 being Element of (b2 . b3)
for b5 being Subset of (product_prebasis b2) st (proj b2,b3) " {b4} c= union b5 & ( for b6 being set st b6 in product_prebasis b2 & b6 in b5 holds
not (proj b2,b3) " {b4} c= b6 ) holds
[#] (product b2) c= union b5
proof end;

theorem Th21: :: YELLOW17:21
for b1 being non empty set
for b2 being non-Empty TopSpace-yielding ManySortedSet of b1
for b3 being Element of b1
for b4 being Subset of (product_prebasis b2) st ( for b5 being finite Subset of b4 holds not [#] (product b2) c= union b5 ) holds
for b5 being Element of (b2 . b3)
for b6 being finite Subset of b4 st (proj b2,b3) " {b5} c= union b6 holds
ex b7 being set st
( b7 in product_prebasis b2 & b7 in b6 & (proj b2,b3) " {b5} c= b7 )
proof end;

theorem Th22: :: YELLOW17:22
for b1 being non empty set
for b2 being non-Empty TopSpace-yielding ManySortedSet of b1
for b3 being Element of b1
for b4 being Subset of (product_prebasis b2) st ( for b5 being finite Subset of b4 holds not [#] (product b2) c= union b5 ) holds
for b5 being Element of (b2 . b3)
for b6 being finite Subset of b4 st (proj b2,b3) " {b5} c= union b6 holds
ex b7 being Subset of (b2 . b3) st
( b7 <> [#] (b2 . b3) & b5 in b7 & (proj b2,b3) " b7 in b6 & b7 is open )
proof end;

theorem Th23: :: YELLOW17:23
for b1 being non empty set
for b2 being non-Empty TopSpace-yielding ManySortedSet of b1
for b3 being Element of b1
for b4 being Subset of (product_prebasis b2) st ( for b5 being Element of b1 holds b2 . b5 is compact ) & ( for b5 being finite Subset of b4 holds not [#] (product b2) c= union b5 ) holds
ex b5 being Element of (b2 . b3) st
for b6 being finite Subset of b4 holds not (proj b2,b3) " {b5} c= union b6
proof end;

theorem Th24: :: YELLOW17:24
for b1 being non empty set
for b2 being non-Empty TopSpace-yielding ManySortedSet of b1 st ( for b3 being Element of b1 holds b2 . b3 is compact ) holds
product b2 is compact
proof end;