:: RELAT_2 semantic presentation
begin
definition
let
R
be ( (
Relation-like
) (
Relation-like
)
Relation
) ;
let
X
be ( ( ) ( )
set
) ;
pred
R
is_reflexive_in
X
means
:: RELAT_2:def 1
for
x
being ( ( ) ( )
set
) st
x
: ( ( ) ( )
set
)
in
X
: ( ( ) ( )
set
) holds
[
x
: ( ( ) ( )
set
) ,
x
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
R
: ( (
Relation-like
) (
Relation-like
)
set
) ;
pred
R
is_irreflexive_in
X
means
:: RELAT_2:def 2
for
x
being ( ( ) ( )
set
) st
x
: ( ( ) ( )
set
)
in
X
: ( ( ) ( )
set
) holds
not
[
x
: ( ( ) ( )
set
) ,
x
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
R
: ( (
Relation-like
) (
Relation-like
)
set
) ;
pred
R
is_symmetric_in
X
means
:: RELAT_2:def 3
for
x
,
y
being ( ( ) ( )
set
) st
x
: ( ( ) ( )
set
)
in
X
: ( ( ) ( )
set
) &
y
: ( ( ) ( )
set
)
in
X
: ( ( ) ( )
set
) &
[
x
: ( ( ) ( )
set
) ,
y
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
R
: ( (
Relation-like
) (
Relation-like
)
set
) holds
[
y
: ( ( ) ( )
set
) ,
x
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
R
: ( (
Relation-like
) (
Relation-like
)
set
) ;
pred
R
is_antisymmetric_in
X
means
:: RELAT_2:def 4
for
x
,
y
being ( ( ) ( )
set
) st
x
: ( ( ) ( )
set
)
in
X
: ( ( ) ( )
set
) &
y
: ( ( ) ( )
set
)
in
X
: ( ( ) ( )
set
) &
[
x
: ( ( ) ( )
set
) ,
y
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
R
: ( (
Relation-like
) (
Relation-like
)
set
) &
[
y
: ( ( ) ( )
set
) ,
x
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
R
: ( (
Relation-like
) (
Relation-like
)
set
) holds
x
: ( ( ) ( )
set
)
=
y
: ( ( ) ( )
set
) ;
pred
R
is_asymmetric_in
X
means
:: RELAT_2:def 5
for
x
,
y
being ( ( ) ( )
set
) st
x
: ( ( ) ( )
set
)
in
X
: ( ( ) ( )
set
) &
y
: ( ( ) ( )
set
)
in
X
: ( ( ) ( )
set
) &
[
x
: ( ( ) ( )
set
) ,
y
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
R
: ( (
Relation-like
) (
Relation-like
)
set
) holds
not
[
y
: ( ( ) ( )
set
) ,
x
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
R
: ( (
Relation-like
) (
Relation-like
)
set
) ;
pred
R
is_connected_in
X
means
:: RELAT_2:def 6
for
x
,
y
being ( ( ) ( )
set
) st
x
: ( ( ) ( )
set
)
in
X
: ( ( ) ( )
set
) &
y
: ( ( ) ( )
set
)
in
X
: ( ( ) ( )
set
) &
x
: ( ( ) ( )
set
)
<>
y
: ( ( ) ( )
set
) & not
[
x
: ( ( ) ( )
set
) ,
y
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
R
: ( (
Relation-like
) (
Relation-like
)
set
) holds
[
y
: ( ( ) ( )
set
) ,
x
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
R
: ( (
Relation-like
) (
Relation-like
)
set
) ;
pred
R
is_strongly_connected_in
X
means
:: RELAT_2:def 7
for
x
,
y
being ( ( ) ( )
set
) st
x
: ( ( ) ( )
set
)
in
X
: ( ( ) ( )
set
) &
y
: ( ( ) ( )
set
)
in
X
: ( ( ) ( )
set
) & not
[
x
: ( ( ) ( )
set
) ,
y
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
R
: ( (
Relation-like
) (
Relation-like
)
set
) holds
[
y
: ( ( ) ( )
set
) ,
x
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
R
: ( (
Relation-like
) (
Relation-like
)
set
) ;
pred
R
is_transitive_in
X
means
:: RELAT_2:def 8
for
x
,
y
,
z
being ( ( ) ( )
set
) st
x
: ( ( ) ( )
set
)
in
X
: ( ( ) ( )
set
) &
y
: ( ( ) ( )
set
)
in
X
: ( ( ) ( )
set
) &
z
: ( ( ) ( )
set
)
in
X
: ( ( ) ( )
set
) &
[
x
: ( ( ) ( )
set
) ,
y
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
R
: ( (
Relation-like
) (
Relation-like
)
set
) &
[
y
: ( ( ) ( )
set
) ,
z
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
R
: ( (
Relation-like
) (
Relation-like
)
set
) holds
[
x
: ( ( ) ( )
set
) ,
z
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
R
: ( (
Relation-like
) (
Relation-like
)
set
) ;
end;
definition
let
R
be ( (
Relation-like
) (
Relation-like
)
Relation
) ;
attr
R
is
reflexive
means
:: RELAT_2:def 9
R
: ( (
Relation-like
) (
Relation-like
)
set
)
is_reflexive_in
field
R
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
) ;
attr
R
is
irreflexive
means
:: RELAT_2:def 10
R
: ( (
Relation-like
) (
Relation-like
)
set
)
is_irreflexive_in
field
R
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
) ;
attr
R
is
symmetric
means
:: RELAT_2:def 11
R
: ( (
Relation-like
) (
Relation-like
)
set
)
is_symmetric_in
field
R
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
) ;
attr
R
is
antisymmetric
means
:: RELAT_2:def 12
R
: ( (
Relation-like
) (
Relation-like
)
set
)
is_antisymmetric_in
field
R
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
) ;
attr
R
is
asymmetric
means
:: RELAT_2:def 13
R
: ( (
Relation-like
) (
Relation-like
)
set
)
is_asymmetric_in
field
R
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
) ;
attr
R
is
connected
means
:: RELAT_2:def 14
R
: ( (
Relation-like
) (
Relation-like
)
set
)
is_connected_in
field
R
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
) ;
attr
R
is
strongly_connected
means
:: RELAT_2:def 15
R
: ( (
Relation-like
) (
Relation-like
)
set
)
is_strongly_connected_in
field
R
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
) ;
attr
R
is
transitive
means
:: RELAT_2:def 16
R
: ( (
Relation-like
) (
Relation-like
)
set
)
is_transitive_in
field
R
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
) ;
end;
registration
cluster
empty
Relation-like
->
Relation-like
reflexive
irreflexive
symmetric
antisymmetric
asymmetric
connected
strongly_connected
transitive
for ( ( ) ( )
set
) ;
end;
theorem
:: RELAT_2:1
for
R
being ( (
Relation-like
) (
Relation-like
)
Relation
) holds
(
R
: ( (
Relation-like
) (
Relation-like
)
Relation
) is
reflexive
iff
id
(
field
R
: ( (
Relation-like
) (
Relation-like
)
Relation
)
)
: ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
field
b
1
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( ( ) ( )
set
)
-defined
field
b
1
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( ( ) ( )
set
)
-valued
)
set
)
c=
R
: ( (
Relation-like
) (
Relation-like
)
Relation
) ) ;
theorem
:: RELAT_2:2
for
R
being ( (
Relation-like
) (
Relation-like
)
Relation
) holds
(
R
: ( (
Relation-like
) (
Relation-like
)
Relation
) is
irreflexive
iff
id
(
field
R
: ( (
Relation-like
) (
Relation-like
)
Relation
)
)
: ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
field
b
1
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( ( ) ( )
set
)
-defined
field
b
1
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( ( ) ( )
set
)
-valued
)
set
)
misses
R
: ( (
Relation-like
) (
Relation-like
)
Relation
) ) ;
theorem
:: RELAT_2:3
for
X
being ( ( ) ( )
set
)
for
R
being ( (
Relation-like
) (
Relation-like
)
Relation
) holds
(
R
: ( (
Relation-like
) (
Relation-like
)
Relation
)
is_antisymmetric_in
X
: ( ( ) ( )
set
) iff
R
: ( (
Relation-like
) (
Relation-like
)
Relation
)
\
(
id
X
: ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
b
1
: ( ( ) ( )
set
)
-valued
)
set
) : ( ( ) (
Relation-like
)
set
)
is_asymmetric_in
X
: ( ( ) ( )
set
) ) ;
theorem
:: RELAT_2:4
for
X
being ( ( ) ( )
set
)
for
R
being ( (
Relation-like
) (
Relation-like
)
Relation
) st
R
: ( (
Relation-like
) (
Relation-like
)
Relation
)
is_asymmetric_in
X
: ( ( ) ( )
set
) holds
R
: ( (
Relation-like
) (
Relation-like
)
Relation
)
\/
(
id
X
: ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
b
1
: ( ( ) ( )
set
)
-valued
)
set
) : ( ( ) (
Relation-like
)
set
)
is_antisymmetric_in
X
: ( ( ) ( )
set
) ;
theorem
:: RELAT_2:5
canceled;
theorem
:: RELAT_2:6
canceled;
theorem
:: RELAT_2:7
canceled;
theorem
:: RELAT_2:8
canceled;
theorem
:: RELAT_2:9
canceled;
theorem
:: RELAT_2:10
canceled;
theorem
:: RELAT_2:11
canceled;
registration
cluster
Relation-like
symmetric
transitive
->
Relation-like
reflexive
for ( ( ) ( )
set
) ;
end;
registration
let
X
be ( ( ) ( )
set
) ;
cluster
id
X
: ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
X
: ( ( ) ( )
set
)
-defined
X
: ( ( ) ( )
set
)
-valued
)
set
)
->
Relation-like
symmetric
antisymmetric
transitive
;
end;
registration
cluster
Relation-like
irreflexive
transitive
->
Relation-like
asymmetric
for ( ( ) ( )
set
) ;
cluster
Relation-like
asymmetric
->
Relation-like
irreflexive
antisymmetric
for ( ( ) ( )
set
) ;
end;
registration
let
R
be ( (
Relation-like
reflexive
) (
Relation-like
reflexive
)
Relation
) ;
cluster
R
: ( (
Relation-like
reflexive
) (
Relation-like
reflexive
)
set
)
~
: ( (
Relation-like
) (
Relation-like
)
set
)
->
Relation-like
reflexive
;
end;
registration
let
R
be ( (
Relation-like
irreflexive
) (
Relation-like
irreflexive
)
Relation
) ;
cluster
R
: ( (
Relation-like
irreflexive
) (
Relation-like
irreflexive
)
set
)
~
: ( (
Relation-like
) (
Relation-like
)
set
)
->
Relation-like
irreflexive
;
end;
theorem
:: RELAT_2:12
for
R
being ( (
Relation-like
) (
Relation-like
)
Relation
) st
R
: ( (
Relation-like
) (
Relation-like
)
Relation
) is
reflexive
holds
(
dom
R
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( ( ) ( )
set
)
=
dom
(
R
: ( (
Relation-like
) (
Relation-like
)
Relation
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
) &
rng
R
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( ( ) ( )
set
)
=
rng
(
R
: ( (
Relation-like
) (
Relation-like
)
Relation
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
) ) ;
theorem
:: RELAT_2:13
for
R
being ( (
Relation-like
) (
Relation-like
)
Relation
) holds
(
R
: ( (
Relation-like
) (
Relation-like
)
Relation
) is
symmetric
iff
R
: ( (
Relation-like
) (
Relation-like
)
Relation
)
=
R
: ( (
Relation-like
) (
Relation-like
)
Relation
)
~
: ( (
Relation-like
) (
Relation-like
)
set
) ) ;
registration
let
P
,
R
be ( (
Relation-like
reflexive
) (
Relation-like
reflexive
)
Relation
) ;
cluster
P
: ( (
Relation-like
reflexive
) (
Relation-like
reflexive
)
set
)
\/
R
: ( (
Relation-like
reflexive
) (
Relation-like
reflexive
)
set
) : ( ( ) (
Relation-like
)
set
)
->
reflexive
;
cluster
P
: ( (
Relation-like
reflexive
) (
Relation-like
reflexive
)
set
)
/\
R
: ( (
Relation-like
reflexive
) (
Relation-like
reflexive
)
set
) : ( ( ) (
Relation-like
)
set
)
->
reflexive
;
end;
registration
let
P
,
R
be ( (
Relation-like
irreflexive
) (
Relation-like
irreflexive
)
Relation
) ;
cluster
P
: ( (
Relation-like
irreflexive
) (
Relation-like
irreflexive
)
set
)
\/
R
: ( (
Relation-like
irreflexive
) (
Relation-like
irreflexive
)
set
) : ( ( ) (
Relation-like
)
set
)
->
irreflexive
;
cluster
P
: ( (
Relation-like
irreflexive
) (
Relation-like
irreflexive
)
set
)
/\
R
: ( (
Relation-like
irreflexive
) (
Relation-like
irreflexive
)
set
) : ( ( ) (
Relation-like
)
set
)
->
irreflexive
;
end;
registration
let
P
be ( (
Relation-like
irreflexive
) (
Relation-like
irreflexive
)
Relation
) ;
let
R
be ( (
Relation-like
) (
Relation-like
)
Relation
) ;
cluster
P
: ( (
Relation-like
irreflexive
) (
Relation-like
irreflexive
)
set
)
\
R
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) (
Relation-like
)
set
)
->
irreflexive
;
end;
registration
let
R
be ( (
Relation-like
symmetric
) (
Relation-like
symmetric
)
Relation
) ;
cluster
R
: ( (
Relation-like
symmetric
) (
Relation-like
symmetric
)
set
)
~
: ( (
Relation-like
) (
Relation-like
)
set
)
->
Relation-like
symmetric
;
end;
registration
let
P
,
R
be ( (
Relation-like
symmetric
) (
Relation-like
symmetric
)
Relation
) ;
cluster
P
: ( (
Relation-like
symmetric
) (
Relation-like
symmetric
)
set
)
\/
R
: ( (
Relation-like
symmetric
) (
Relation-like
symmetric
)
set
) : ( ( ) (
Relation-like
)
set
)
->
symmetric
;
cluster
P
: ( (
Relation-like
symmetric
) (
Relation-like
symmetric
)
set
)
/\
R
: ( (
Relation-like
symmetric
) (
Relation-like
symmetric
)
set
) : ( ( ) (
Relation-like
)
set
)
->
symmetric
;
cluster
P
: ( (
Relation-like
symmetric
) (
Relation-like
symmetric
)
set
)
\
R
: ( (
Relation-like
symmetric
) (
Relation-like
symmetric
)
set
) : ( ( ) (
Relation-like
)
set
)
->
symmetric
;
end;
registration
let
R
be ( (
Relation-like
asymmetric
) (
Relation-like
irreflexive
antisymmetric
asymmetric
)
Relation
) ;
cluster
R
: ( (
Relation-like
asymmetric
) (
Relation-like
irreflexive
antisymmetric
asymmetric
)
set
)
~
: ( (
Relation-like
) (
Relation-like
irreflexive
)
set
)
->
Relation-like
asymmetric
;
end;
registration
let
P
be ( (
Relation-like
) (
Relation-like
)
Relation
) ;
let
R
be ( (
Relation-like
asymmetric
) (
Relation-like
irreflexive
antisymmetric
asymmetric
)
Relation
) ;
cluster
P
: ( (
Relation-like
) (
Relation-like
)
set
)
/\
R
: ( (
Relation-like
asymmetric
) (
Relation-like
irreflexive
antisymmetric
asymmetric
)
set
) : ( ( ) (
Relation-like
)
set
)
->
asymmetric
;
cluster
R
: ( (
Relation-like
asymmetric
) (
Relation-like
irreflexive
antisymmetric
asymmetric
)
set
)
/\
P
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) (
Relation-like
)
set
)
->
asymmetric
;
end;
registration
let
P
be ( (
Relation-like
asymmetric
) (
Relation-like
irreflexive
antisymmetric
asymmetric
)
Relation
) ;
let
R
be ( (
Relation-like
) (
Relation-like
)
Relation
) ;
cluster
P
: ( (
Relation-like
asymmetric
) (
Relation-like
irreflexive
antisymmetric
asymmetric
)
set
)
\
R
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) (
Relation-like
irreflexive
)
set
)
->
asymmetric
;
end;
theorem
:: RELAT_2:14
canceled;
theorem
:: RELAT_2:15
canceled;
theorem
:: RELAT_2:16
canceled;
theorem
:: RELAT_2:17
canceled;
theorem
:: RELAT_2:18
canceled;
theorem
:: RELAT_2:19
canceled;
theorem
:: RELAT_2:20
canceled;
theorem
:: RELAT_2:21
canceled;
theorem
:: RELAT_2:22
for
R
being ( (
Relation-like
) (
Relation-like
)
Relation
) holds
(
R
: ( (
Relation-like
) (
Relation-like
)
Relation
) is
antisymmetric
iff
R
: ( (
Relation-like
) (
Relation-like
)
Relation
)
/\
(
R
: ( (
Relation-like
) (
Relation-like
)
Relation
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) (
Relation-like
)
set
)
c=
id
(
dom
R
: ( (
Relation-like
) (
Relation-like
)
Relation
)
)
: ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
dom
b
1
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( ( ) ( )
set
)
-defined
dom
b
1
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( ( ) ( )
set
)
-valued
reflexive
symmetric
antisymmetric
transitive
)
set
) ) ;
registration
let
R
be ( (
Relation-like
antisymmetric
) (
Relation-like
antisymmetric
)
Relation
) ;
cluster
R
: ( (
Relation-like
antisymmetric
) (
Relation-like
antisymmetric
)
set
)
~
: ( (
Relation-like
) (
Relation-like
)
set
)
->
Relation-like
antisymmetric
;
end;
registration
let
P
be ( (
Relation-like
antisymmetric
) (
Relation-like
antisymmetric
)
Relation
) ;
let
R
be ( (
Relation-like
) (
Relation-like
)
Relation
) ;
cluster
P
: ( (
Relation-like
antisymmetric
) (
Relation-like
antisymmetric
)
set
)
/\
R
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) (
Relation-like
)
set
)
->
antisymmetric
;
cluster
R
: ( (
Relation-like
) (
Relation-like
)
set
)
/\
P
: ( (
Relation-like
antisymmetric
) (
Relation-like
antisymmetric
)
set
) : ( ( ) (
Relation-like
)
set
)
->
antisymmetric
;
cluster
P
: ( (
Relation-like
antisymmetric
) (
Relation-like
antisymmetric
)
set
)
\
R
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) (
Relation-like
)
set
)
->
antisymmetric
;
end;
registration
let
R
be ( (
Relation-like
transitive
) (
Relation-like
transitive
)
Relation
) ;
cluster
R
: ( (
Relation-like
transitive
) (
Relation-like
transitive
)
set
)
~
: ( (
Relation-like
) (
Relation-like
)
set
)
->
Relation-like
transitive
;
end;
registration
let
P
,
R
be ( (
Relation-like
transitive
) (
Relation-like
transitive
)
Relation
) ;
cluster
P
: ( (
Relation-like
transitive
) (
Relation-like
transitive
)
set
)
/\
R
: ( (
Relation-like
transitive
) (
Relation-like
transitive
)
set
) : ( ( ) (
Relation-like
)
set
)
->
transitive
;
end;
theorem
:: RELAT_2:23
canceled;
theorem
:: RELAT_2:24
canceled;
theorem
:: RELAT_2:25
canceled;
theorem
:: RELAT_2:26
canceled;
theorem
:: RELAT_2:27
for
R
being ( (
Relation-like
) (
Relation-like
)
Relation
) holds
(
R
: ( (
Relation-like
) (
Relation-like
)
Relation
) is
transitive
iff
R
: ( (
Relation-like
) (
Relation-like
)
Relation
)
*
R
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( (
Relation-like
) (
Relation-like
)
set
)
c=
R
: ( (
Relation-like
) (
Relation-like
)
Relation
) ) ;
theorem
:: RELAT_2:28
for
R
being ( (
Relation-like
) (
Relation-like
)
Relation
) holds
(
R
: ( (
Relation-like
) (
Relation-like
)
Relation
) is
connected
iff
[:
(
field
R
: ( (
Relation-like
) (
Relation-like
)
Relation
)
)
: ( ( ) ( )
set
) ,
(
field
R
: ( (
Relation-like
) (
Relation-like
)
Relation
)
)
: ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
)
\
(
id
(
field
R
: ( (
Relation-like
) (
Relation-like
)
Relation
)
)
: ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
field
b
1
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( ( ) ( )
set
)
-defined
field
b
1
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( ( ) ( )
set
)
-valued
reflexive
symmetric
antisymmetric
transitive
)
set
) : ( ( ) (
Relation-like
)
set
)
c=
R
: ( (
Relation-like
) (
Relation-like
)
Relation
)
\/
(
R
: ( (
Relation-like
) (
Relation-like
)
Relation
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) (
Relation-like
)
set
) ) ;
registration
cluster
Relation-like
strongly_connected
->
Relation-like
reflexive
connected
for ( ( ) ( )
set
) ;
end;
theorem
:: RELAT_2:29
canceled;
theorem
:: RELAT_2:30
for
R
being ( (
Relation-like
) (
Relation-like
)
Relation
) holds
(
R
: ( (
Relation-like
) (
Relation-like
)
Relation
) is
strongly_connected
iff
[:
(
field
R
: ( (
Relation-like
) (
Relation-like
)
Relation
)
)
: ( ( ) ( )
set
) ,
(
field
R
: ( (
Relation-like
) (
Relation-like
)
Relation
)
)
: ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
)
=
R
: ( (
Relation-like
) (
Relation-like
)
Relation
)
\/
(
R
: ( (
Relation-like
) (
Relation-like
)
Relation
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) (
Relation-like
)
set
) ) ;
theorem
:: RELAT_2:31
for
R
being ( (
Relation-like
) (
Relation-like
)
Relation
) holds
(
R
: ( (
Relation-like
) (
Relation-like
)
Relation
) is
transitive
iff for
x
,
y
,
z
being ( ( ) ( )
set
) st
[
x
: ( ( ) ( )
set
) ,
y
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
R
: ( (
Relation-like
) (
Relation-like
)
Relation
) &
[
y
: ( ( ) ( )
set
) ,
z
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
R
: ( (
Relation-like
) (
Relation-like
)
Relation
) holds
[
x
: ( ( ) ( )
set
) ,
z
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
R
: ( (
Relation-like
) (
Relation-like
)
Relation
) ) ;