for b₁ being set ex b₂ being set st
( b₁ in b₂ & ( for b₃, b₄ being set st b₃ in b₂ & b₄ c= b₃ holds
b₄ in b₂ ) & ( for b₃ being set st b₃ in b₂ holds
bool b₃ in b₂ ) & ( for b₃ being set holds
( not b₃ c= b₂ or b₃,b₂ are_equipotent or b₃ in b₂ ) ) )

proof end;

Lemma2: :: SUBSET_1:lemma 3
for b₁ being set
for b₂ being Subset of b₁
for b₃ being set st b₃ in b₂ holds
b₃ in b₁

proof end;

theorem Th43: :: SUBSET_1:43

for b₁ being set
for b₂, b₃ being Subset of b₁ holds
( b₂ misses b₃ iff b₂ c= b₃ ` )

proof end;

theorem Th50: :: SUBSET_1:50

for b₁ being set st b₁ <> {} holds
for b₂ being Subset of b₁
for b₃ being Element of b₁ st not b₃ in b₂ holds
b₃ in b₂ `

proof end;

theorem Th54: :: SUBSET_1:54

for b₁, b₂ being set
for b₃ being Subset of b₁ st b₂ in b₃ ` holds
not b₂ in b₃ by XBOOLE_0:def 4;

Lemma11: :: SUBSET_1:lemma 71
for b₁, b₂ being set st ( for b₃ being set st b₃ in b₁ holds
b₃ in b₂ ) holds
b₁ is Subset of b₂

proof end;

theorem Th46: :: SETFAM_1:46

for b₁ being set
for b₂ being Subset-Family of b₁ st b₂ <> {} holds
COMPLEMENT b₂ <> {}

proof end;

theorem Th47: :: SETFAM_1:47

for b₁ being set
for b₂ being Subset-Family of b₁ st b₂ <> {} holds
([#] b₁) \ (union b₂) = meet (COMPLEMENT b₂)

proof end;

theorem Th48: :: SETFAM_1:48

for b₁ being set
for b₂ being Subset-Family of b₁ st b₂ <> {} holds
union (COMPLEMENT b₂) = ([#] b₁) \ (meet b₂)

proof end;

theorem Th20: :: RELAT_1:20

for b₁, b₂ being set
for b₃ being Relation st [b₁,b₂] in b₃ holds
( b₁ in dom b₃ & b₂ in rng b₃ ) by Def4, Def5;

theorem Th21: :: RELAT_1:21

for b₁ being Relation holds b₁ c= [:(dom b₁),(rng b₁):]

proof end;

theorem Th25: :: RELAT_1:25

for b₁, b₂ being Relation st b₁ c= b₂ holds
( dom b₁ c= dom b₂ & rng b₁ c= rng b₂ )

proof end;

theorem Th30: :: RELAT_1:30

for b₁, b₂ being set
for b₃ being Relation st [b₁,b₂] in b₃ holds
( b₁ in field b₃ & b₂ in field b₃ )

proof end;

theorem Th37: :: RELAT_1:37

for b₁ being Relation holds
( rng b₁ = dom (b₁ ~ ) & dom b₁ = rng (b₁ ~ ) )

proof end;

theorem Th44: :: RELAT_1:44

for b₁, b₂ being Relation holds dom (b₁ * b₂) c= dom b₁

proof end;

theorem Th45: :: RELAT_1:45

for b₁, b₂ being Relation holds rng (b₁ * b₂) c= rng b₂

proof end;

theorem Th46: :: RELAT_1:46

for b₁, b₂ being Relation st rng b₁ c= dom b₂ holds
dom (b₁ * b₂) = dom b₁

proof end;

theorem Th47: :: RELAT_1:47

for b₁, b₂ being Relation st dom b₁ c= rng b₂ holds
rng (b₂ * b₁) = rng b₁

proof end;

theorem Th56: :: RELAT_1:56

for b₁ being Relation st ( for b₂, b₃ being set holds not [b₂,b₃] in b₁ ) holds
b₁ = {}

proof end;

theorem Th60: :: RELAT_1:60

( dom {} = {} & rng {} = {} )

proof end;

theorem Th64: :: RELAT_1:64

for b₁ being Relation st ( dom b₁ = {} or rng b₁ = {} ) holds
b₁ = {}

proof end;

theorem Th65: :: RELAT_1:65

for b₁ being Relation holds
( dom b₁ = {} iff rng b₁ = {} ) by Th60, Th64;

theorem Th71: :: RELAT_1:71

for b₁ being set holds
( dom (id b₁) = b₁ & rng (id b₁) = b₁ )

proof end;

theorem Th74: :: RELAT_1:74

for b₁, b₂, b₃ being set
for b₄ being Relation holds
( [b₁,b₂] in (id b₃) * b₄ iff ( b₁ in b₃ & [b₁,b₂] in b₄ ) )

proof end;

theorem Th86: :: RELAT_1:86

for b₁, b₂ being set
for b₃ being Relation holds
( b₁ in dom (b₃ | b₂) iff ( b₁ in b₂ & b₁ in dom b₃ ) )

proof end;

theorem Th88: :: RELAT_1:88

for b₁ being set
for b₂ being Relation holds b₂ | b₁ c= b₂

proof end;

theorem Th90: :: RELAT_1:90

for b₁ being set
for b₂ being Relation holds dom (b₂ | b₁) = (dom b₂) /\ b₁

proof end;

theorem Th94: :: RELAT_1:94

for b₁ being set
for b₂ being Relation holds b₂ | b₁ = (id b₁) * b₂

proof end;

theorem Th99: :: RELAT_1:99

for b₁ being set
for b₂ being Relation holds rng (b₂ | b₁) c= rng b₂

proof end;

theorem Th115: :: RELAT_1:115

for b₁, b₂ being set
for b₃ being Relation holds
( b₁ in rng (b₂ | b₃) iff ( b₁ in b₂ & b₁ in rng b₃ ) )

proof end;

theorem Th116: :: RELAT_1:116

for b₁ being set
for b₂ being Relation holds rng (b₁ | b₂) c= b₁

proof end;

theorem Th117: :: RELAT_1:117

for b₁ being set
for b₂ being Relation holds b₁ | b₂ c= b₂

proof end;

theorem Th118: :: RELAT_1:118

for b₁ being set
for b₂ being Relation holds rng (b₁ | b₂) c= rng b₂

proof end;

theorem Th119: :: RELAT_1:119

for b₁ being set
for b₂ being Relation holds rng (b₁ | b₂) = (rng b₂) /\ b₁

proof end;

theorem Th140: :: RELAT_1:140

for b₁, b₂ being set
for b₃ being Relation holds (b₁ | b₃) | b₂ = b₁ | (b₃ | b₂)

proof end;

theorem Th143: :: RELAT_1:143

for b₁, b₂ being set
for b₃ being Relation holds
( b₁ in b₃ .: b₂ iff ex b₄ being set st
( b₄ in dom b₃ & [b₄,b₁] in b₃ & b₄ in b₂ ) )

proof end;

theorem Th144: :: RELAT_1:144

for b₁ being set
for b₂ being Relation holds b₂ .: b₁ c= rng b₂

proof end;

theorem Th145: :: RELAT_1:145

for b₁ being set
for b₂ being Relation holds b₂ .: b₁ = b₂ .: ((dom b₂) /\ b₁)

proof end;

theorem Th146: :: RELAT_1:146

for b₁ being Relation holds b₁ .: (dom b₁) = rng b₁

proof end;

theorem Th160: :: RELAT_1:160

for b₁, b₂ being Relation holds rng (b₁ * b₂) = b₂ .: (rng b₁)

proof end;

theorem Th166: :: RELAT_1:166

for b₁, b₂ being set
for b₃ being Relation holds
( b₁ in b₃ " b₂ iff ex b₄ being set st
( b₄ in rng b₃ & [b₁,b₄] in b₃ & b₄ in b₂ ) )

proof end;

theorem Th167: :: RELAT_1:167

for b₁ being set
for b₂ being Relation holds b₂ " b₁ c= dom b₂

proof end;

theorem Th174: :: RELAT_1:174

for b₁ being set
for b₂ being Relation st b₁ <> {} & b₁ c= rng b₂ holds
b₂ " b₁ <> {}

proof end;

theorem Th178: :: RELAT_1:178

for b₁, b₂ being set
for b₃ being Relation st b₁ c= b₂ holds
b₃ " b₁ c= b₃ " b₂

proof end;

theorem Th8: :: FUNCT_1:8

for b₁, b₂ being set
for b₃ being Function holds
( [b₁,b₂] in b₃ iff ( b₁ in dom b₃ & b₂ = b₃ . b₁ ) )

proof end;

theorem Th21: :: FUNCT_1:21

for b₁ being set
for b₂, b₃ being Function holds
( b₁ in dom (b₂ * b₃) iff ( b₁ in dom b₃ & b₃ . b₁ in dom b₂ ) )

proof end;

theorem Th22: :: FUNCT_1:22

for b₁ being set
for b₂, b₃ being Function st b₁ in dom (b₂ * b₃) holds
(b₂ * b₃) . b₁ = b₂ . (b₃ . b₁)

proof end;

theorem Th23: :: FUNCT_1:23

for b₁ being set
for b₂, b₃ being Function st b₁ in dom b₂ holds
(b₃ * b₂) . b₁ = b₃ . (b₂ . b₁)

proof end;

theorem Th34: :: FUNCT_1:34

for b₁ being set
for b₂ being Function holds
( b₂ = id b₁ iff ( dom b₂ = b₁ & ( for b₃ being set st b₃ in b₁ holds
b₂ . b₃ = b₃ ) ) )

proof end;

theorem Th35: :: FUNCT_1:35

for b₁, b₂ being set st b₂ in b₁ holds
(id b₁) . b₂ = b₂ by Th34;

theorem Th54: :: FUNCT_1:54

for b₁ being Function st b₁ is one-to-one holds
for b₂ being Function holds
( b₂ = b₁ " iff ( dom b₂ = rng b₁ & ( for b₃, b₄ being set holds
( b₃ in rng b₁ & b₄ = b₂ . b₃ iff ( b₄ in dom b₁ & b₃ = b₁ . b₄ ) ) ) ) )

proof end;

theorem Th55: :: FUNCT_1:55

for b₁ being Function st b₁ is one-to-one holds
( rng b₁ = dom (b₁ " ) & dom b₁ = rng (b₁ " ) )

proof end;

theorem Th57: :: FUNCT_1:57

for b₁ being set
for b₂ being Function st b₂ is one-to-one & b₁ in rng b₂ holds
( b₁ = b₂ . ((b₂ " ) . b₁) & b₁ = (b₂ * (b₂ " )) . b₁ )

proof end;

theorem Th62: :: FUNCT_1:62

for b₁ being Function st b₁ is one-to-one holds
b₁ " is one-to-one

proof end;

theorem Th68: :: FUNCT_1:68

for b₁ being set
for b₂, b₃ being Function holds
( b₂ = b₃ | b₁ iff ( dom b₂ = (dom b₃) /\ b₁ & ( for b₄ being set st b₄ in dom b₂ holds
b₂ . b₄ = b₃ . b₄ ) ) )

proof end;

theorem Th70: :: FUNCT_1:70

for b₁, b₂ being set
for b₃ being Function st b₂ in dom (b₃ | b₁) holds
(b₃ | b₁) . b₂ = b₃ . b₂ by Th68;

Lemma30: :: FUNCT_1:lemma 82
for b₁, b₂ being set
for b₃ being Function holds
( b₂ in dom (b₃ | b₁) iff ( b₂ in dom b₃ & b₂ in b₁ ) )

proof end;

theorem Th72: :: FUNCT_1:72

for b₁, b₂ being set
for b₃ being Function st b₂ in b₁ holds
(b₃ | b₁) . b₂ = b₃ . b₂

proof end;

theorem Th145: :: FUNCT_1:145

for b₁ being set
for b₂ being Function holds b₂ .: (b₂ " b₁) c= b₁

proof end;

theorem Th146: :: FUNCT_1:146

for b₁ being set
for b₂ being Relation st b₁ c= dom b₂ holds
b₁ c= b₂ " (b₂ .: b₁)

proof end;

theorem Th147: :: FUNCT_1:147

for b₁ being set
for b₂ being Function st b₁ c= rng b₂ holds
b₂ .: (b₂ " b₁) = b₁

proof end;

theorem Th3: :: ORDINAL1:3

for b₁, b₂, b₃ being set holds
( not b₁ in b₂ or not b₂ in b₃ or not b₃ in b₁ )

proof end;

theorem Th10: :: ORDINAL1:10

for b₁ being set holds b₁ in succ b₁

proof end;

theorem Th21: :: ORDINAL1:21

for b₁ being epsilon-transitive set
for b₂ being Ordinal st b₁ c< b₂ holds
b₁ in b₂

proof end;

theorem Th23: :: ORDINAL1:23

for b₁ being set
for b₂ being Ordinal st b₁ in b₂ holds
b₁ is Ordinal

proof end;

theorem Th24: :: ORDINAL1:24

for b₁, b₂ being Ordinal holds
( b₁ in b₂ or b₁ = b₂ or b₂ in b₁ )

proof end;

theorem Th31: :: ORDINAL1:31

for b₁ being set st ( for b₂ being set st b₂ in b₁ holds
( b₂ is Ordinal & b₂ c= b₁ ) ) holds
b₁ is ordinal

proof end;

theorem Th32: :: ORDINAL1:32

for b₁ being set
for b₂ being Ordinal st b₁ c= b₂ & b₁ <> {} holds
ex b₃ being Ordinal st
( b₃ in b₁ & ( for b₄ being Ordinal st b₄ in b₁ holds
b₃ c= b₄ ) )

proof end;

theorem Th33: :: ORDINAL1:33

for b₁, b₂ being Ordinal holds
( b₁ in b₂ iff succ b₁ c= b₂ )

proof end;

theorem Th41: :: ORDINAL1:41

for b₁ being Ordinal holds
( b₁ is_limit_ordinal iff for b₂ being Ordinal st b₂ in b₁ holds
succ b₂ in b₁ )

proof end;

theorem Th42: :: ORDINAL1:42

for b₁ being Ordinal holds
( not b₁ is_limit_ordinal iff ex b₂ being Ordinal st b₁ = succ b₂ )

proof end;

Lemma1: :: WELLORD1:lemma 1
for b₁ being Relation holds
( b₁ is reflexive iff for b₂ being set st b₂ in field b₁ holds
[b₂,b₂] in b₁ )

proof end;

Lemma2: :: WELLORD1:lemma 2
for b₁ being Relation holds
( b₁ is transitive iff for b₂, b₃, b₄ being set st [b₂,b₃] in b₁ & [b₃,b₄] in b₁ holds
[b₂,b₄] in b₁ )

proof end;

Lemma3: :: WELLORD1:lemma 3
for b₁ being Relation holds
( b₁ is antisymmetric iff for b₂, b₃ being set st [b₂,b₃] in b₁ & [b₃,b₂] in b₁ holds
b₂ = b₃ )

proof end;

Lemma4: :: WELLORD1:lemma 4
for b₁ being Relation holds
( b₁ is connected iff for b₂, b₃ being set st b₂ in field b₁ & b₃ in field b₁ & b₂ <> b₃ & not [b₂,b₃] in b₁ holds
[b₃,b₂] in b₁ )

proof end;

theorem Th5: :: WELLORD1:5

for b₁ being Relation holds
( b₁ is well_founded iff b₁ is_well_founded_in field b₁ )

proof end;

theorem Th8: :: WELLORD1:8

for b₁ being Relation holds
( b₁ well_orders field b₁ iff b₁ is well-ordering )

proof end;

theorem Th16: :: WELLORD1:16

for b₁, b₂ being set
for b₃ being Relation holds
( b₁ in b₃ |_2 b₂ iff ( b₁ in b₃ & b₁ in [:b₂,b₂:] ) ) by XBOOLE_0:def 3;

theorem Th17: :: WELLORD1:17

for b₁ being set
for b₂ being Relation holds b₂ |_2 b₁ = (b₁ | b₂) | b₁

proof end;

theorem Th18: :: WELLORD1:18

for b₁ being set
for b₂ being Relation holds b₂ |_2 b₁ = b₁ | (b₂ | b₁)

proof end;

Lemma17: :: WELLORD1:lemma 29
for b₁ being set
for b₂ being Relation holds dom (b₁ | b₂) c= dom b₂

proof end;

theorem Th19: :: WELLORD1:19

for b₁, b₂ being set
for b₃ being Relation st b₁ in field (b₃ |_2 b₂) holds
( b₁ in field b₃ & b₁ in b₂ )

proof end;

theorem Th20: :: WELLORD1:20

for b₁ being set
for b₂ being Relation holds
( field (b₂ |_2 b₁) c= field b₂ & field (b₂ |_2 b₁) c= b₁ )

proof end;

theorem Th21: :: WELLORD1:21

for b₁, b₂ being set
for b₃ being Relation holds (b₃ |_2 b₁) -Seg b₂ c= b₃ -Seg b₂

proof end;

theorem Th22: :: WELLORD1:22

for b₁ being set
for b₂ being Relation st b₂ is reflexive holds
b₂ |_2 b₁ is reflexive

proof end;

theorem Th23: :: WELLORD1:23

for b₁ being set
for b₂ being Relation st b₂ is connected holds
b₂ |_2 b₁ is connected

proof end;

theorem Th24: :: WELLORD1:24

for b₁ being set
for b₂ being Relation st b₂ is transitive holds
b₂ |_2 b₁ is transitive

proof end;

theorem Th25: :: WELLORD1:25

for b₁ being set
for b₂ being Relation st b₂ is antisymmetric holds
b₂ |_2 b₁ is antisymmetric

proof end;

theorem Th31: :: WELLORD1:31

for b₁ being set
for b₂ being Relation st b₂ is well_founded holds
b₂ |_2 b₁ is well_founded

proof end;

theorem Th32: :: WELLORD1:32

for b₁ being set
for b₂ being Relation st b₂ is well-ordering holds
b₂ |_2 b₁ is well-ordering

proof end;

theorem Th39: :: WELLORD1:39

for b₁ being set
for b₂ being Relation st b₂ is well-ordering & b₁ c= field b₂ holds
field (b₂ |_2 b₁) = b₁

proof end;

theorem Th49: :: WELLORD1:49

for b₁, b₂ being Relation
for b₃ being Function st b₃ is_isomorphism_of b₁,b₂ holds
b₃ " is_isomorphism_of b₂,b₁

proof end;

theorem Th53: :: WELLORD1:53

for b₁, b₂ being Relation
for b₃ being Function st b₃ is_isomorphism_of b₁,b₂ holds
( ( b₁ is reflexive implies b₂ is reflexive ) & ( b₁ is transitive implies b₂ is transitive ) & ( b₁ is connected implies b₂ is connected ) & ( b₁ is antisymmetric implies b₂ is antisymmetric ) & ( b₁ is well_founded implies b₂ is well_founded ) )

proof end;

theorem Th54: :: WELLORD1:54

for b₁, b₂ being Relation
for b₃ being Function st b₁ is well-ordering & b₃ is_isomorphism_of b₁,b₂ holds
b₂ is well-ordering

proof end;

theorem Th12: :: RELSET_1:12

for b₁, b₂ being set
for b₃ being Relation of b₁,b₂ holds
( dom b₃ c= b₁ & rng b₃ c= b₂ )

proof end;

theorem Th14: :: RELSET_1:14

for b₁, b₂, b₃ being set
for b₄ being Relation of b₃,b₁ st rng b₄ c= b₂ holds
b₄ is Relation of b₃,b₂

proof end;

theorem Th16: :: RELSET_1:16

for b₁, b₂, b₃ being set
for b₄ being Relation of b₃,b₁ st b₁ c= b₂ holds
b₄ is Relation of b₃,b₂

proof end;

theorem Th22: :: RELSET_1:22

for b₁, b₂ being set
for b₃ being Relation of b₂,b₁ holds
( ( for b₄ being set st b₄ in b₂ holds
ex b₅ being set st [b₄,b₅] in b₃ ) iff dom b₃ = b₂ )

proof end;

theorem Th23: :: RELSET_1:23

for b₁, b₂ being set
for b₃ being Relation of b₁,b₂ holds
( ( for b₄ being set st b₄ in b₂ holds
ex b₅ being set st [b₅,b₄] in b₃ ) iff rng b₃ = b₂ )

proof end;

theorem Th7: :: MCART_1:7

for b₁, b₂ being set holds
( [b₁,b₂] `1 = b₁ & [b₁,b₂] `2 = b₂ ) by Def1, Def2;

theorem Th2: :: WELLORD2:2

for b₁ being set holds RelIncl b₁ is reflexive

proof end;

theorem Th3: :: WELLORD2:3

for b₁ being set holds RelIncl b₁ is transitive

proof end;

theorem Th4: :: WELLORD2:4

for b₁ being Ordinal holds RelIncl b₁ is connected

proof end;

theorem Th5: :: WELLORD2:5

for b₁ being set holds RelIncl b₁ is antisymmetric

proof end;

theorem Th6: :: WELLORD2:6

for b₁ being Ordinal holds RelIncl b₁ is well_founded

proof end;

theorem Th7: :: WELLORD2:7

for b₁ being Ordinal holds RelIncl b₁ is well-ordering

proof end;

theorem Th25: :: WELLORD2:25

for b₁ being set
for b₂ being Relation st b₂ well_orders b₁ holds
( field (b₂ |_2 b₁) = b₁ & b₂ |_2 b₁ is well-ordering )

proof end;

Lemma17: :: WELLORD2:lemma 30
for b₁ being set
for b₂ being Relation st b₂ is well-ordering & b₁, field b₂ are_equipotent holds
ex b₃ being Relation st b₃ well_orders b₁

proof end;

theorem Th26: :: WELLORD2:26

for b₁ being set ex b₂ being Relation st b₂ well_orders b₁

proof end;

theorem Th28: :: WELLORD2:28

for b₁ being non empty set st ( for b₂ being set st b₂ in b₁ holds
b₂ <> {} ) holds
ex b₂ being Function st
( dom b₂ = b₁ & ( for b₃ being set st b₃ in b₁ holds
b₂ . b₃ in b₃ ) )

proof end;

theorem Th6: :: FUNCT_2:6

for b₁, b₂, b₃ being set
for b₄ being Function of b₁,b₂ st b₂ <> {} & b₃ in b₁ holds
b₄ . b₃ in rng b₄

proof end;

theorem Th9: :: FUNCT_2:9

for b₁, b₂, b₃ being set
for b₄ being Function of b₁,b₂ st ( b₂ = {} implies b₁ = {} ) & b₂ c= b₃ holds
b₄ is Function of b₁,b₃

proof end;

theorem Th21: :: FUNCT_2:21

for b₁, b₂, b₃ being set
for b₄ being Function of b₁,b₂
for b₅ being Function st b₂ <> {} & b₃ in b₁ holds
(b₅ * b₄) . b₃ = b₅ . (b₄ . b₃)

proof end;

theorem Th46: :: FUNCT_2:46

for b₁, b₂, b₃ being set
for b₄ being Function of b₁,b₂ st b₂ <> {} holds
for b₅ being set holds
( b₅ in b₄ " b₃ iff ( b₅ in b₁ & b₄ . b₅ in b₃ ) )

proof end;

theorem Th13: :: FINSET_1:13

for b₁, b₂ being set st b₁ c= b₂ & b₂ is finite holds
b₁ is finite

proof end;

theorem Th15: :: FINSET_1:15

for b₁, b₂ being set st b₁ is finite holds
b₁ /\ b₂ is finite

proof end;

theorem Th17: :: FINSET_1:17

for b₁ being set
for b₂ being Function st b₁ is finite holds
b₂ .: b₁ is finite

proof end;

theorem Th18: :: FINSET_1:18

for b₁ being set st b₁ is finite holds
for b₂ being Subset-Family of b₁ st b₂ <> {} holds
ex b₃ being set st
( b₃ in b₂ & ( for b₄ being set st b₄ in b₂ & b₃ c= b₄ holds
b₄ = b₃ ) )

proof end;

theorem Th26: :: FINSET_1:26

for b₁ being Function st dom b₁ is finite holds
rng b₁ is finite

proof end;

theorem Th23: :: LATTICES:23

for b₁ being non empty meet-commutative meet-absorbing LattStr
for b₂, b₃ being Element of b₁ holds b₂ "/\" b₃ [= b₂

proof end;

theorem Th26: :: LATTICES:26

for b₁ being non empty join-commutative \/-SemiLattStr
for b₂, b₃ being Element of b₁ st b₂ [= b₃ & b₃ [= b₂ holds
b₂ = b₃

proof end;

theorem Th12: :: PRE_TOPC:12

for b₁ being 1-sorted holds [#] b₁ = the carrier of b₁ ;

theorem Th15: :: PRE_TOPC:15

for b₁ being 1-sorted
for b₂ being Subset of b₁ holds b₂ /\ ([#] b₁) = b₂ by XBOOLE_1:28;

theorem Th17: :: PRE_TOPC:17

for b₁ being 1-sorted
for b₂ being Subset of b₁ holds b₂ ` = ([#] b₁) \ b₂ by SUBSET_1:def 5;

theorem Th22: :: PRE_TOPC:22

for b₁ being 1-sorted
for b₂ being Subset of b₁ holds ([#] b₁) \ (([#] b₁) \ b₂) = b₂

proof end;

theorem Th44: :: PRE_TOPC:44

for b₁ being TopSpace
for b₂ being Subset-Family of b₁ st ( for b₃ being Subset of b₁ st b₃ in b₂ holds
b₃ is closed ) holds
meet b₂ is closed

proof end;

theorem Th45: :: PRE_TOPC:45

for b₁ being TopStruct
for b₂ being Subset of b₁
for b₃ being set st b₃ in the carrier of b₁ holds
( b₃ in Cl b₂ iff for b₄ being Subset of b₁ st b₄ is closed & b₂ c= b₄ holds
b₃ in b₄ )

proof end;

theorem Th46: :: PRE_TOPC:46

for b₁ being TopSpace
for b₂ being Subset of b₁ ex b₃ being Subset-Family of b₁ st
( ( for b₄ being Subset of b₁ holds
( b₄ in b₃ iff ( b₄ is closed & b₂ c= b₄ ) ) ) & Cl b₂ = meet b₃ )

proof end;

theorem Th48: :: PRE_TOPC:48

for b₁ being TopStruct
for b₂ being Subset of b₁ holds b₂ c= Cl b₂

proof end;

theorem Th52: :: PRE_TOPC:52

for b₁ being TopStruct
for b₂ being Subset of b₁ holds
( ( b₂ is closed implies Cl b₂ = b₂ ) & ( b₁ is TopSpace-like & Cl b₂ = b₂ implies b₂ is closed ) )

proof end;

theorem Th29: :: TOPS_1:29

for b₁ being TopStruct
for b₂ being Subset of b₁ holds
( b₂ is closed iff b₂ ` is open )

proof end;

theorem Th30: :: TOPS_1:30

for b₁ being TopStruct
for b₂ being Subset of b₁ holds
( b₂ is open iff b₂ ` is closed )

proof end;

Lemma15: :: TOPS_1:lemma 40
for b₁ being non empty 1-sorted
for b₂ being Subset of b₁
for b₃ being Element of b₁ holds
( b₃ in b₂ ` iff not b₃ in b₂ ) by SUBSET_1:50, SUBSET_1:54;

theorem Th44: :: TOPS_1:44

for b₁ being TopStruct
for b₂ being Subset of b₁ holds Int b₂ c= b₂

proof end;

theorem Th51: :: TOPS_1:51

for b₁ being TopSpace
for b₂ being Subset of b₁ holds Int b₂ is open ;

theorem Th55: :: TOPS_1:55

for b₁ being TopSpace
for b₂ being TopStruct
for b₃ being Subset of b₁
for b₄ being Subset of b₂ holds
( ( b₄ is open implies Int b₄ = b₄ ) & ( Int b₃ = b₃ implies b₃ is open ) )

proof end;

theorem Th5: :: TOPS_2:5

for b₁ being non empty 1-sorted
for b₂ being Subset-Family of b₁ st b₂ is_a_cover_of b₁ holds
b₂ <> {}

proof end;

theorem Th10: :: TOPS_2:10

for b₁ being set
for b₂ being Subset-Family of b₁ holds
( b₂ <> {} iff COMPLEMENT b₂ <> {} )

proof end;

theorem Th11: :: TOPS_2:11

for b₁ being set
for b₂ being Subset-Family of b₁ st b₂ <> {} holds
meet (COMPLEMENT b₂) = (union b₂) `

proof end;

theorem Th12: :: TOPS_2:12

for b₁ being set
for b₂ being Subset-Family of b₁ st b₂ <> {} holds
union (COMPLEMENT b₂) = (meet b₂) `

proof end;

theorem Th13: :: TOPS_2:13

for b₁ being 1-sorted
for b₂ being Subset-Family of b₁ holds
( COMPLEMENT b₂ is finite iff b₂ is finite )

proof end;

theorem Th16: :: TOPS_2:16

for b₁ being TopStruct
for b₂ being Subset-Family of b₁ holds
( b₂ is closed iff COMPLEMENT b₂ is open )

proof end;

theorem Th17: :: TOPS_2:17

for b₁ being TopStruct
for b₂ being Subset-Family of b₁ holds
( b₂ is open iff COMPLEMENT b₂ is closed )

proof end;

theorem Th13: :: COMPTS_1:13

for b₁ being non empty TopSpace holds
( b₁ is compact iff for b₂ being Subset-Family of b₁ st b₂ is centered & b₂ is closed holds
meet b₂ <> {} )

proof end;

theorem Th25: :: ORDERS_2:25

for b₁ being antisymmetric RelStr
for b₂, b₃ being Element of b₁ st b₂ <= b₃ & b₃ <= b₂ holds
b₂ = b₃

proof end;

theorem Th26: :: ORDERS_2:26

for b₁ being transitive RelStr
for b₂, b₃, b₄ being Element of b₁ st b₂ <= b₃ & b₃ <= b₄ holds
b₂ <= b₄

proof end;

theorem Th5: :: CONNSP_2:5

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Point of b₁ st b₂ is open & b₃ in b₂ holds
b₂ is a_neighborhood of b₃

proof end;

theorem Th32: :: FILTER_1:32

for b₁ being Lattice
for b₂, b₃ being Element of b₁ holds
( [b₂,b₃] in LattRel b₁ iff b₂ [= b₃ )

proof end;

theorem Th1: :: LATTICE3:1

for b₁ being set
for b₂, b₃ being Element of (BooleLatt b₁) holds
( b₂ "\/" b₃ = b₂ \/ b₃ & b₂ "/\" b₃ = b₂ /\ b₃ )

proof end;

theorem Th2: :: LATTICE3:2

for b₁ being set
for b₂, b₃ being Element of (BooleLatt b₁) holds
( b₂ [= b₃ iff b₂ c= b₃ )

proof end;

theorem Th3: :: LATTICE3:3

for b₁ being set holds
( BooleLatt b₁ is lower-bounded & Bottom (BooleLatt b₁) = {} )

proof end;

theorem Th7: :: LATTICE3:7

for b₁ being Lattice
for b₂, b₃ being Element of b₁ holds
( b₂ [= b₃ iff b₂ % <= b₃ % )

proof end;

theorem Th28: :: LATTICE3:28

for b₁ being set
for b₂ being Lattice
for b₃ being Element of b₂ holds
( b₃ is_less_than b₁ iff b₃ % is_<=_than b₁ )

proof end;

theorem Th29: :: LATTICE3:29

for b₁ being set
for b₂ being Lattice
for b₃ being Element of (LattPOSet b₂) holds
( b₃ is_<=_than b₁ iff % b₃ is_less_than b₁ )

proof end;

theorem Th30: :: LATTICE3:30

for b₁ being set
for b₂ being Lattice
for b₃ being Element of b₂ holds
( b₁ is_less_than b₃ iff b₁ is_<=_than b₃ % )

proof end;

theorem Th31: :: LATTICE3:31

for b₁ being set
for b₂ being Lattice
for b₃ being Element of (LattPOSet b₂) holds
( b₁ is_<=_than b₃ iff b₁ is_less_than % b₃ )

proof end;

theorem Th34: :: LATTICE3:34

for b₁ being complete Lattice
for b₂ being Element of b₁
for b₃ being set holds
( b₂ = "/\" b₃,b₁ iff ( b₂ is_less_than b₃ & ( for b₄ being Element of b₁ st b₄ is_less_than b₃ holds
b₄ [= b₂ ) ) )

proof end;

theorem Th50: :: LATTICE3:50

for b₁ being complete Lattice holds
( b₁ is 0_Lattice & Bottom b₁ = "\/" {} ,b₁ )

proof end;

theorem Th91: :: TMAP_1:91

for b₁ being non empty 1-sorted
for b₂ being Element of b₁ holds (id b₁) . b₂ = b₂

proof end;

theorem Th5: :: TEX_2:5

for b₁ being set
for b₂ being Subset of b₁ holds
( b₂ is proper iff b₂ <> b₁ )

proof end;

theorem Th6: :: YELLOW_0:6

for b₁ being RelStr
for b₂ being Element of b₁ holds
( {} is_<=_than b₂ & {} is_>=_than b₂ )

proof end;

theorem Th15: :: YELLOW_0:15

for b₁ being antisymmetric RelStr
for b₂ being set holds
( ex_sup_of b₂,b₁ iff ex b₃ being Element of b₁ st
( b₂ is_<=_than b₃ & ( for b₄ being Element of b₁ st b₂ is_<=_than b₄ holds
b₃ <= b₄ ) ) )

proof end;

theorem Th16: :: YELLOW_0:16

for b₁ being antisymmetric RelStr
for b₂ being set holds
( ex_inf_of b₂,b₁ iff ex b₃ being Element of b₁ st
( b₂ is_>=_than b₃ & ( for b₄ being Element of b₁ st b₂ is_>=_than b₄ holds
b₃ >= b₄ ) ) )

proof end;

theorem Th29: :: YELLOW_0:29

for b₁ being complete Lattice
for b₂ being set holds
( "\/" b₂,b₁ = "\/" b₂,(LattPOSet b₁) & "/\" b₂,b₁ = "/\" b₂,(LattPOSet b₁) )

proof end;

theorem Th30: :: YELLOW_0:30

for b₁ being antisymmetric RelStr
for b₂ being Element of b₁
for b₃ being set holds
( b₂ = "\/" b₃,b₁ & ex_sup_of b₃,b₁ iff ( b₂ is_>=_than b₃ & ( for b₄ being Element of b₁ st b₄ is_>=_than b₃ holds
b₂ <= b₄ ) ) )

proof end;

theorem Th42: :: YELLOW_0:42

for b₁ being non empty antisymmetric lower-bounded RelStr holds
( ex_sup_of {} ,b₁ & ex_inf_of the carrier of b₁,b₁ )

proof end;

theorem Th44: :: YELLOW_0:44

for b₁ being non empty antisymmetric lower-bounded RelStr
for b₂ being Element of b₁ holds Bottom b₁ <= b₂

proof end;

theorem Th60: :: YELLOW_0:60

for b₁ being RelStr
for b₂ being SubRelStr of b₁
for b₃, b₄ being Element of b₁
for b₅, b₆ being Element of b₂ st b₅ = b₃ & b₆ = b₄ & b₅ <= b₆ holds
b₃ <= b₄

proof end;

theorem Th61: :: YELLOW_0:61

for b₁ being RelStr
for b₂ being full SubRelStr of b₁
for b₃, b₄ being Element of b₁
for b₅, b₆ being Element of b₂ st b₅ = b₃ & b₆ = b₄ & b₃ <= b₄ & b₅ in the carrier of b₂ & b₆ in the carrier of b₂ holds
b₅ <= b₆

proof end;

theorem Th1: :: WAYBEL_0:1

for b₁ being non empty transitive RelStr
for b₂ being Subset of b₁ holds
( ( not b₂ is empty & b₂ is directed ) iff for b₃ being finite Subset of b₂ ex b₄ being Element of b₁ st
( b₄ in b₂ & b₄ is_>=_than b₃ ) )

proof end;

theorem Th8: :: WAYBEL_0:8

for b₁ being non empty 1-sorted
for b₂ being non empty NetStr of b₁
for b₃, b₄ being set st b₃ c= b₄ holds
( ( b₂ is_eventually_in b₃ implies b₂ is_eventually_in b₄ ) & ( b₂ is_often_in b₃ implies b₂ is_often_in b₄ ) )

proof end;

theorem Th1: :: YELLOW_1:1

for b₁ being set holds
( the carrier of (InclPoset b₁) = b₁ & the InternalRel of (InclPoset b₁) = RelIncl b₁ ) ;

theorem Th2: :: YELLOW_1:2

for b₁ being set
for b₂, b₃ being Element of (BoolePoset b₁) holds
( b₂ <= b₃ iff b₂ c= b₃ )

proof end;

theorem Th4: :: YELLOW_1:4

for b₁ being set holds BoolePoset b₁ = InclPoset (bool b₁)

proof end;

theorem Th18: :: YELLOW_1:18

for b₁ being set holds Bottom (BoolePoset b₁) = {}

proof end;

theorem Th6: :: YELLOW_6:6

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Point of b₁ holds
( b₃ in Cl b₂ iff for b₄ being a_neighborhood of b₃ holds b₄ meets b₂ )

proof end;

theorem Th19: :: YELLOW_6:19

for b₁ being 1-sorted
for b₂ being NetStr of b₁
for b₃ being SubNetStr of b₂ holds the carrier of b₃ c= the carrier of b₂

proof end;

theorem Th20: :: YELLOW_6:20

for b₁ being 1-sorted
for b₂ being NetStr of b₁
for b₃ being SubNetStr of b₂
for b₄, b₅ being Element of b₂
for b₆, b₇ being Element of b₃ st b₄ = b₆ & b₅ = b₇ & b₆ <= b₇ holds
b₄ <= b₅

proof end;

theorem Th21: :: YELLOW_6:21

for b₁ being 1-sorted
for b₂ being non empty NetStr of b₁
for b₃ being non empty full SubNetStr of b₂
for b₄, b₅ being Element of b₂
for b₆, b₇ being Element of b₃ st b₄ = b₆ & b₅ = b₇ & b₄ <= b₅ holds
b₆ <= b₇

proof end;

theorem Th28: :: YELLOW_6:28

for b₁ being non empty 1-sorted
for b₂ being net of b₁
for b₃ being set st b₂ is_eventually_in b₃ holds
b₂ is_often_in b₃

proof end;

theorem Th30: :: YELLOW_6:30

for b₁ being non empty 1-sorted
for b₂ being net of b₁
for b₃ being set st b₂ is_often_in b₃ holds
( not b₂ " b₃ is empty & b₂ " b₃ is directed )

proof end;

theorem Th31: :: YELLOW_6:31

for b₁ being non empty 1-sorted
for b₂ being net of b₁
for b₃ being set st b₂ is_often_in b₃ holds
b₂ " b₃ is subnet of b₂

proof end;

theorem Th32: :: YELLOW_6:32

for b₁ being non empty 1-sorted
for b₂ being net of b₁
for b₃ being set
for b₄ being subnet of b₂ st b₄ = b₂ " b₃ holds
b₄ is_eventually_in b₃

proof end;

theorem Th41: :: YELLOW_6:41

for b₁ being non empty TopSpace
for b₂ being net of b₁
for b₃ being subnet of b₂ holds Lim b₂ c= Lim b₃

proof end;

theorem Th11: :: WAYBEL_7:11

for b₁ being set
for b₂ being Subset of (BoolePoset b₁) holds
( b₂ is upper iff for b₃, b₄ being set st b₃ c= b₄ & b₄ c= b₁ & b₃ in b₂ holds
b₄ in b₂ )

proof end;

theorem Th4: :: WAYBEL_7:4

for b₁ being set holds the carrier of (BoolePoset b₁) = bool b₁

proof end;

theorem Th8: :: WAYBEL_7:8

for b₁ being non empty lower-bounded Poset
for b₂ being Filter of b₁ holds
( b₂ is proper iff not Bottom b₁ in b₂ )

proof end;

theorem Th12: :: WAYBEL_9:12

for b₁ being non empty 1-sorted
for b₂ being non empty NetStr of b₁
for b₃ being Element of b₂ holds the carrier of (b₂ | b₃) = { b₄ where B is Element of b₂ : b₃ <= b₄ }

proof end;

theorem Th16: :: WAYBEL_9:16

for b₁ being non empty 1-sorted
for b₂ being non empty directed NetStr of b₁
for b₃, b₄ being Element of b₂
for b₅ being Element of (b₂ | b₃) st b₄ = b₅ holds
b₂ . b₄ = (b₂ | b₃) . b₅

proof end;

theorem Th29: :: WAYBEL_9:29

for b₁ being non empty TopSpace
for b₂ being net of b₁
for b₃ being Point of b₁ st b₃ in Lim b₂ holds
b₃ is_a_cluster_point_of b₂

proof end;

theorem Th2: :: YELLOW19:2

for b₁ being non empty set
for b₂ being proper Filter of (BoolePoset b₁)
for b₃ being set st b₃ in b₂ holds
not b₃ is empty

proof end;

theorem Th3: :: YELLOW19:3

for b₁ being non empty TopSpace
for b₂ being Point of b₁
for b₃ being set holds
( b₃ in NeighborhoodSystem b₂ iff b₃ is a_neighborhood of b₂ )

proof end;

theorem Th4: :: YELLOW19:4

for b₁ being non empty TopSpace
for b₂ being Point of b₁
for b₃ being upper Subset of (BoolePoset ([#] b₁)) holds
( b₂ is_a_convergence_point_of b₃,b₁ iff NeighborhoodSystem b₂ c= b₃ )

proof end;

theorem Th9: :: YELLOW19:9

for b₁ being non empty 1-sorted
for b₂ being net of b₁
for b₃ being Subset of b₁,b₂ holds b₂ is_eventually_in b₃

proof end;

theorem Th11: :: YELLOW19:11

for b₁ being non empty 1-sorted
for b₂ being non empty NetStr of b₁
for b₃ being set holds
( b₃ in a_filter b₂ iff ( b₂ is_eventually_in b₃ & b₃ is Subset of b₁ ) )

proof end;

theorem Th13: :: YELLOW19:13

for b₁ being non empty TopSpace
for b₂ being net of b₁
for b₃ being Point of b₁ holds
( b₃ in Lim b₂ iff b₃ is_a_convergence_point_of a_filter b₂,b₁ )

proof end;

theorem Th14: :: YELLOW19:14

for b₁ being non empty 1-sorted
for b₂ being Filter of (BoolePoset ([#] b₁)) holds b₂ \ {{} } = a_filter (a_net b₂)

proof end;

theorem Th15: :: YELLOW19:15

for b₁ being non empty 1-sorted
for b₂ being proper Filter of (BoolePoset ([#] b₁)) holds b₂ = a_filter (a_net b₂)

proof end;

theorem Th18: :: YELLOW19:18

for b₁ being non empty TopSpace
for b₂ being proper Filter of (BoolePoset ([#] b₁))
for b₃ being Point of b₁ holds
( b₃ in Lim (a_net b₂) iff b₃ is_a_convergence_point_of b₂,b₁ )

proof end;

theorem Th20: :: YELLOW19:20

for b₁ being non empty TopSpace
for b₂ being Point of b₁
for b₃ being Subset of b₁ st b₂ in Cl b₃ holds
for b₄ being proper Filter of (BoolePoset ([#] b₁)) st b₄ = NeighborhoodSystem b₂ holds
a_net b₄ is_often_in b₃

proof end;

theorem Th23: :: YELLOW19:23

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Point of b₁ holds
( b₃ in Cl b₂ iff ex b₄ being net of b₁ st
( b₄ is_eventually_in b₂ & b₃ is_a_cluster_point_of b₄ ) )

proof end;

theorem Th31: :: YELLOW19:31

for b₁ being non empty TopSpace
for b₂ being net of b₁
for b₃ being Point of b₁ holds
( b₃ is_a_cluster_point_of b₂ iff for b₄ being Subset of b₁,b₂ holds b₃ in Cl b₄ )

proof end;

Lemma24: :: YELLOW19:lemma 37
for b₁ being non empty TopSpace st b₁ is compact holds
for b₂ being net of b₁ ex b₃ being Point of b₁ st b₃ is_a_cluster_point_of b₂

proof end;