begin
definition
let R be
Relation;
let X be
set ;
pred R is_reflexive_in X means :
Def1:
for
x being
set st
x in X holds
[x,x] in R;
pred R is_irreflexive_in X means :
Def2:
for
x being
set st
x in X holds
not
[x,x] in R;
pred R is_symmetric_in X means :
Def3:
for
x,
y being
set st
x in X &
y in X &
[x,y] in R holds
[y,x] in R;
pred R is_antisymmetric_in X means :
Def4:
for
x,
y being
set st
x in X &
y in X &
[x,y] in R &
[y,x] in R holds
x = y;
pred R is_asymmetric_in X means :
Def5:
for
x,
y being
set st
x in X &
y in X &
[x,y] in R holds
not
[y,x] in R;
pred R is_connected_in X means :
Def6:
for
x,
y being
set st
x in X &
y in X &
x <> y & not
[x,y] in R holds
[y,x] in R;
pred R is_strongly_connected_in X means :
Def7:
for
x,
y being
set st
x in X &
y in X & not
[x,y] in R holds
[y,x] in R;
pred R is_transitive_in X means :
Def8:
for
x,
y,
z being
set st
x in X &
y in X &
z in X &
[x,y] in R &
[y,z] in R holds
[x,z] in R;
end;
:: deftheorem Def1 defines is_reflexive_in RELAT_2:def 1 :
:: deftheorem Def2 defines is_irreflexive_in RELAT_2:def 2 :
:: deftheorem Def3 defines is_symmetric_in RELAT_2:def 3 :
:: deftheorem Def4 defines is_antisymmetric_in RELAT_2:def 4 :
:: deftheorem Def5 defines is_asymmetric_in RELAT_2:def 5 :
:: deftheorem Def6 defines is_connected_in RELAT_2:def 6 :
:: deftheorem Def7 defines is_strongly_connected_in RELAT_2:def 7 :
:: deftheorem Def8 defines is_transitive_in RELAT_2:def 8 :
:: deftheorem Def9 defines reflexive RELAT_2:def 9 :
:: deftheorem Def10 defines irreflexive RELAT_2:def 10 :
:: deftheorem Def11 defines symmetric RELAT_2:def 11 :
:: deftheorem Def12 defines antisymmetric RELAT_2:def 12 :
:: deftheorem Def13 defines asymmetric RELAT_2:def 13 :
:: deftheorem Def14 defines connected RELAT_2:def 14 :
:: deftheorem Def15 defines strongly_connected RELAT_2:def 15 :
:: deftheorem Def16 defines transitive RELAT_2:def 16 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
canceled;
theorem Th22:
theorem Th23:
theorem
theorem
theorem
theorem Th27:
theorem
theorem
theorem Th30:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem