let c₁, c₂ be set ;
let c₃ be Relation of c₁,c₂;
let c₄ be Element of c₁;
func c₃ .: c₄ -> Subset of a₂ equals :: RELSET_2:def 1
a₃ .: {a₄};
correctness ;

end;

:: deftheorem Def1 defines .: RELSET_2:def 1 :

theorem Th9: :: RELSET_2:9

for b₁, b₂ being set
for b₃ being Relation holds
( b₁ in b₃ .: {b₂} iff [b₂,b₁] in b₃ )

proof end;

theorem Th10: :: RELSET_2:10

for b₁ being set
for b₂, b₃ being Relation holds (b₂ \/ b₃) .: {b₁} = (b₂ .: {b₁}) \/ (b₃ .: {b₁})

proof end;

theorem Th11: :: RELSET_2:11

for b₁ being set
for b₂, b₃ being Relation holds (b₂ /\ b₃) .: {b₁} = (b₂ .: {b₁}) /\ (b₃ .: {b₁})

proof end;

theorem Th12: :: RELSET_2:12

for b₁ being set
for b₂, b₃ being Relation holds (b₂ \ b₃) .: {b₁} = (b₂ .: {b₁}) \ (b₃ .: {b₁})

proof end;

theorem Th13: :: RELSET_2:13

for b₁ being set
for b₂, b₃ being Relation holds (b₂ /\ b₃) .: {_{b₁}_} c= (b₂ .: {_{b₁}_}) /\ (b₃ .: {_{b₁}_})

proof end;

definition

let c₁, c₂ be set ;
let c₃ be Relation of c₁,c₂;
let c₄ be Element of c₁;
func c₃ " c₄ -> Subset of a₁ equals :: RELSET_2:def 2
a₃ " {a₄};
correctness ;

end;

:: deftheorem Def2 defines " RELSET_2:def 2 :

theorem Th14: :: RELSET_2:14

for b₁ being set
for b₂ being Subset-Family of b₁
for b₃ being Relation holds b₃ .: (union b₂) = union { (b₃ .: b₄) where B is Subset of b₁ : b₄ in b₂ }

proof end;

theorem Th15: :: RELSET_2:15

for b₁ being non empty set
for b₂ being Subset of b₁ holds b₂ = union { {b₃} where B is Element of b₁ : b₃ in b₂ }

proof end;

theorem Th16: :: RELSET_2:16

for b₁ being non empty set
for b₂ being Subset of b₁ holds { {b₃} where B is Element of b₁ : b₃ in b₂ } is Subset-Family of b₁

proof end;

theorem Th17: :: RELSET_2:17

for b₁ being non empty set
for b₂ being set
for b₃ being Subset of b₁
for b₄ being Relation of b₁,b₂ holds b₄ .: b₃ = union { (b₄ .: b₅) where B is Element of b₁ : b₅ in b₃ }

proof end;

theorem Th18: :: RELSET_2:18

for b₁ being non empty set
for b₂ being set
for b₃ being Subset of b₁
for b₄ being Relation of b₁,b₂ holds { (b₄ .: b₅) where B is Element of b₁ : b₅ in b₃ } is Subset-Family of b₂

proof end;

definition

let c₁, c₂ be set ;
let c₃ be Subset of [:c₁,(bool c₂):];
let c₄ be set ;
redefine func .: as c₃ .: c₄ -> Subset-Family of a₂;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be Relation;
func .: c₂,c₁ -> Function means :Def3: :: RELSET_2:def 3
( dom a₃ = bool a₁ & ( for b₁ being set st b₁ c= a₁ holds
a₃ . b₁ = a₂ .: b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines .: RELSET_2:def 3 :

notation

let c₁, c₂ be set ;
let c₃ be Subset of [:c₂,c₁:];
synonym .: c₃ for .: c₂,c₁;

end;

theorem Th19: :: RELSET_2:19

for b₁, b₂, b₃ being set
for b₄ being Subset of [:b₂,b₃:] st b₁ in dom (.: ) holds
(.: ) . b₁ = b₄ .: b₁

proof end;

theorem Th20: :: RELSET_2:20

for b₁, b₂ being set
for b₃ being Subset of [:b₁,b₂:] holds rng (.: ) c= bool (rng b₃)

proof end;

theorem Th21: :: RELSET_2:21

for b₁, b₂ being set
for b₃ being Subset of [:b₁,b₂:] holds .: is Function of bool b₁, bool (rng b₃)

proof end;

definition

let c₁, c₂ be set ;
let c₃ be Subset of [:c₂,c₁:];
redefine func .: as .: c₃ -> Function of bool a₂, bool a₁;
correctness

proof end;

end;

theorem Th22: :: RELSET_2:22

for b₁, b₂ being set
for b₃ being Subset of [:b₁,b₂:] holds union ((.: b₃) .: b₁) c= b₃ .: (union b₁)

proof end;

definition

let c₁, c₂ be set ;
let c₃ be Subset of c₁;
let c₄ be Subset of [:c₁,c₂:];
func c₄ .:^ c₃ -> set equals :: RELSET_2:def 4
Intersect ((.: a₄) .: {_{a₃}_});
correctness ;

end;

:: deftheorem Def4 defines .:^ RELSET_2:def 4 :

definition

let c₁, c₂ be set ;
let c₃ be Subset of c₁;
let c₄ be Subset of [:c₁,c₂:];
redefine func .:^ as c₄ .:^ c₃ -> Subset of a₂;
coherence ;

end;

theorem Th23: :: RELSET_2:23

for b₁, b₂ being set
for b₃ being Subset of b₁
for b₄ being Subset of [:b₁,b₂:] holds
( (.: b₄) .: {_{b₃}_} = {} iff b₃ = {} )

proof end;

theorem Th24: :: RELSET_2:24

for b₁, b₂, b₃ being set
for b₄ being Subset of b₁
for b₅ being Subset of [:b₁,b₂:] st b₃ in b₅ .:^ b₄ holds
for b₆ being set st b₆ in b₄ holds
b₃ in b₅ .: {b₆}

proof end;

theorem Th25: :: RELSET_2:25

for b₁ being non empty set
for b₂ being set
for b₃ being Subset of b₂
for b₄ being Element of b₁
for b₅ being Subset of [:b₂,b₁:] holds
( b₄ in b₅ .:^ b₃ iff for b₆ being set st b₆ in b₃ holds
b₄ in b₅ .: {b₆} )

proof end;

theorem Th26: :: RELSET_2:26

for b₁, b₂ being set
for b₃, b₄ being Subset of b₁
for b₅ being Subset of [:b₁,b₂:] st (.: b₅) .: {_{b₃}_} = {} holds
b₅ .:^ (b₃ \/ b₄) = b₅ .:^ b₄

proof end;

theorem Th27: :: RELSET_2:27

for b₁, b₂ being set
for b₃, b₄ being Subset of b₁
for b₅ being Subset of [:b₁,b₂:] holds b₅ .:^ (b₃ \/ b₄) = (b₅ .:^ b₃) /\ (b₅ .:^ b₄)

proof end;

theorem Th28: :: RELSET_2:28

for b₁ being non empty set
for b₂ being set
for b₃ being Subset-Family of b₁
for b₄ being Relation of b₁,b₂ holds { (b₄ .:^ b₅) where B is Subset of b₁ : b₅ in b₃ } is Subset-Family of b₂

proof end;

theorem Th29: :: RELSET_2:29

for b₁, b₂ being set
for b₃ being Subset of b₁
for b₄ being Subset of [:b₁,b₂:] st b₃ = {} holds
b₄ .:^ b₃ = b₂

proof end;

theorem Th30: :: RELSET_2:30

for b₁ being set
for b₂ being Subset-Family of b₁ holds
( union b₂ = {} iff for b₃ being set st b₃ in b₂ holds
b₃ = {} )

proof end;

theorem Th31: :: RELSET_2:31

for b₁ being set
for b₂ being non empty set
for b₃ being Relation of b₁,b₂
for b₄ being Subset-Family of b₁
for b₅ being Subset-Family of b₂ st b₅ = { (b₃ .:^ b₆) where B is Subset of b₁ : b₆ in b₄ } holds
b₃ .:^ (union b₄) = Intersect b₅

proof end;

theorem Th32: :: RELSET_2:32

for b₁, b₂ being set
for b₃, b₄ being Subset of b₁
for b₅ being Subset of [:b₁,b₂:] st b₃ c= b₄ holds
b₅ .:^ b₄ c= b₅ .:^ b₃

proof end;

theorem Th33: :: RELSET_2:33

for b₁, b₂ being set
for b₃, b₄ being Subset of b₁
for b₅ being Subset of [:b₁,b₂:] holds (b₅ .:^ b₃) \/ (b₅ .:^ b₄) c= b₅ .:^ (b₃ /\ b₄)

proof end;

theorem Th34: :: RELSET_2:34

for b₁, b₂ being set
for b₃ being Subset of b₁
for b₄, b₅ being Subset of [:b₁,b₂:] holds (b₄ /\ b₅) .:^ b₃ = (b₄ .:^ b₃) /\ (b₅ .:^ b₃)

proof end;

theorem Th35: :: RELSET_2:35

for b₁, b₂ being set
for b₃ being Subset of b₁
for b₄ being Subset-Family of [:b₁,b₂:] holds (union b₄) .: b₃ = union { (b₅ .: b₃) where B is Subset of [:b₁,b₂:] : b₅ in b₄ }

proof end;

theorem Th36: :: RELSET_2:36

for b₁, b₂ being set
for b₃ being Subset-Family of [:b₁,b₂:]
for b₄, b₅ being set
for b₆ being Subset of b₄ holds { (b₇ .:^ b₆) where B is Subset of [:b₄,b₅:] : b₇ in b₃ } is Subset-Family of b₅

proof end;

theorem Th37: :: RELSET_2:37

for b₁, b₂ being set
for b₃ being Subset of b₁
for b₄ being Subset of [:b₁,b₂:] st b₄ = {} & b₃ <> {} holds
b₄ .:^ b₃ = {}

proof end;

theorem Th38: :: RELSET_2:38

for b₁, b₂ being set
for b₃ being Subset of b₁
for b₄ being Subset of [:b₁,b₂:] st b₄ = [:b₁,b₂:] holds
b₄ .:^ b₃ = b₂

proof end;

theorem Th39: :: RELSET_2:39

for b₁, b₂ being set
for b₃ being Subset of b₂
for b₄ being Subset-Family of [:b₂,b₁:]
for b₅ being Subset-Family of b₁ st b₅ = { (b₆ .:^ b₃) where B is Subset of [:b₂,b₁:] : b₆ in b₄ } holds
(Intersect b₄) .:^ b₃ = Intersect b₅

proof end;

theorem Th40: :: RELSET_2:40

for b₁, b₂ being set
for b₃ being Subset of b₁
for b₄, b₅ being Subset of [:b₁,b₂:] st b₄ c= b₅ holds
b₄ .:^ b₃ c= b₅ .:^ b₃

proof end;

theorem Th41: :: RELSET_2:41

for b₁, b₂ being set
for b₃ being Subset of b₁
for b₄, b₅ being Subset of [:b₁,b₂:] holds (b₄ .:^ b₃) \/ (b₅ .:^ b₃) c= (b₄ \/ b₅) .:^ b₃

proof end;

theorem Th42: :: RELSET_2:42

for b₁, b₂, b₃, b₄ being set
for b₅ being Subset of [:b₃,b₄:] holds
( b₁ in (b₅ ` ) .: {b₂} iff ( not [b₂,b₁] in b₅ & b₂ in b₃ & b₁ in b₄ ) )

proof end;

theorem Th43: :: RELSET_2:43

for b₁, b₂ being set
for b₃ being Subset of b₁
for b₄ being Subset of [:b₁,b₂:] st b₃ <> {} holds
b₄ .:^ b₃ c= b₄ .: b₃

proof end;

theorem Th44: :: RELSET_2:44

for b₁, b₂ being set
for b₃ being Subset of [:b₁,b₂:]
for b₄, b₅ being set holds
( b₄ meets (b₃ ~ ) .: b₅ iff ex b₆, b₇ being set st
( b₆ in b₄ & b₇ in b₅ & b₆ in (b₃ ~ ) .: {b₇} ) )

proof end;

theorem Th45: :: RELSET_2:45

for b₁, b₂ being set
for b₃ being Subset of [:b₁,b₂:]
for b₄, b₅ being set holds
( ex b₆, b₇ being set st
( b₆ in b₄ & b₇ in b₅ & b₆ in (b₃ ~ ) .: {b₇} ) iff b₅ meets b₃ .: b₄ )

proof end;

theorem Th46: :: RELSET_2:46

for b₁, b₂ being set
for b₃ being Subset of b₁
for b₄ being Subset of b₂
for b₅ being Subset of [:b₁,b₂:] holds
( b₃ misses (b₅ ~ ) .: b₄ iff b₄ misses b₅ .: b₃ )

proof end;

theorem Th47: :: RELSET_2:47

for b₁, b₂ being set
for b₃ being Subset of [:b₁,b₂:]
for b₄ being set holds b₃ .: b₄ = b₃ .: (b₄ /\ (proj1 b₃))

proof end;

theorem Th48: :: RELSET_2:48

for b₁, b₂ being set
for b₃ being Subset of [:b₁,b₂:]
for b₄ being set holds (b₃ ~ ) .: b₄ = (b₃ ~ ) .: (b₄ /\ (proj2 b₃))

proof end;

theorem Th49: :: RELSET_2:49

for b₁, b₂ being set
for b₃ being Subset of b₁
for b₄ being Subset of [:b₁,b₂:] holds (b₄ .:^ b₃) ` = (b₄ ` ) .: b₃

proof end;

definition

let c₁, c₂, c₃ be set ;
let c₄ be Subset of [:c₁,c₂:];
let c₅ be Subset of [:c₂,c₃:];
redefine func * as c₄ * c₅ -> Relation of a₁,a₃;
coherence

proof end;

end;

theorem Th50: :: RELSET_2:50

for b₁, b₂ being set
for b₃ being Subset of b₁
for b₄ being Relation of b₁,b₂ holds (b₄ .: b₃) ` = (b₄ ` ) .:^ b₃

proof end;

theorem Th51: :: RELSET_2:51

for b₁, b₂ being set
for b₃ being Relation of b₂,b₁ holds
( proj1 b₃ = (b₃ ~ ) .: b₁ & proj2 b₃ = b₃ .: b₂ )

proof end;

theorem Th52: :: RELSET_2:52

for b₁, b₂, b₃ being set
for b₄ being Relation of b₁,b₂
for b₅ being Relation of b₂,b₃ holds
( proj1 (b₄ * b₅) = (b₄ ~ ) .: (proj1 b₅) & proj1 (b₄ * b₅) c= proj1 b₄ )

proof end;

theorem Th53: :: RELSET_2:53

for b₁, b₂, b₃ being set
for b₄ being Relation of b₁,b₂
for b₅ being Relation of b₂,b₃ holds
( proj2 (b₄ * b₅) = b₅ .: (proj2 b₄) & proj2 (b₄ * b₅) c= proj2 b₅ )

proof end;

theorem Th54: :: RELSET_2:54

for b₁, b₂ being set
for b₃ being Subset of b₁
for b₄ being Relation of b₁,b₂ holds
( b₃ c= proj1 b₄ iff b₃ c= (b₄ * (b₄ ~ )) .: b₃ )

proof end;

theorem Th55: :: RELSET_2:55

for b₁, b₂ being set
for b₃ being Subset of b₂
for b₄ being Relation of b₁,b₂ holds
( b₃ c= proj2 b₄ iff b₃ c= ((b₄ ~ ) * b₄) .: b₃ )

proof end;

theorem Th56: :: RELSET_2:56

for b₁, b₂ being set
for b₃ being Relation of b₂,b₁ holds
( proj1 b₃ = (b₃ ~ ) .: b₁ & (b₃ ~ ) .: (b₃ .: b₂) = (b₃ ~ ) .: (proj2 b₃) ) by Th51;

theorem Th57: :: RELSET_2:57

for b₁, b₂ being set
for b₃ being Relation of b₂,b₁ holds (b₃ ~ ) .: b₁ = (b₃ * (b₃ ~ )) .: b₂

proof end;

theorem Th58: :: RELSET_2:58

for b₁, b₂ being set
for b₃ being Relation of b₁,b₂ holds b₃ .: b₁ = ((b₃ ~ ) * b₃) .: b₂

proof end;

theorem Th59: :: RELSET_2:59

for b₁, b₂, b₃ being set
for b₄ being Subset of b₁
for b₅ being Relation of b₁,b₂
for b₆ being Relation of b₂,b₃ holds b₆ .:^ (b₅ .: b₄) = ((b₅ * (b₆ ` )) ` ) .:^ b₄

proof end;

theorem Th60: :: RELSET_2:60

for b₁, b₂ being set
for b₃ being Relation of b₁,b₂ holds (b₃ ` ) ~ = (b₃ ~ ) `

proof end;

theorem Th61: :: RELSET_2:61

for b₁, b₂ being set
for b₃ being Subset of b₁
for b₄ being Subset of b₂
for b₅ being Relation of b₁,b₂ holds
( b₃ c= (b₅ ~ ) .:^ b₄ iff b₄ c= b₅ .:^ b₃ )

proof end;

theorem Th62: :: RELSET_2:62

for b₁, b₂ being set
for b₃ being Subset of b₁
for b₄ being Subset of b₂
for b₅ being Relation of b₁,b₂ holds
( b₅ .: (b₃ ` ) c= b₄ ` iff (b₅ ~ ) .: b₄ c= b₃ )

proof end;

theorem Th63: :: RELSET_2:63

for b₁, b₂ being set
for b₃ being Subset of b₁
for b₄ being Subset of b₂
for b₅ being Relation of b₁,b₂ holds
( b₃ c= (b₅ ~ ) .:^ (b₅ .:^ b₃) & b₄ c= b₅ .:^ ((b₅ ~ ) .:^ b₄) ) by Th61;

theorem Th64: :: RELSET_2:64

for b₁, b₂ being set
for b₃ being Subset of b₁
for b₄ being Subset of b₂
for b₅ being Relation of b₁,b₂ holds
( b₅ .:^ b₃ = b₅ .:^ ((b₅ ~ ) .:^ (b₅ .:^ b₃)) & (b₅ ~ ) .:^ b₄ = (b₅ ~ ) .:^ (b₅ .:^ ((b₅ ~ ) .:^ b₄)) )

proof end;

theorem Th65: :: RELSET_2:65

for b₁, b₂ being set
for b₃ being Relation of b₁,b₂ holds (id b₁) * b₃ = b₃ * (id b₂)

proof end;