begin
Lm1:
for R being Relation holds
( R is reflexive iff for x being set st x in field R holds
[x,x] in R )
Lm2:
for R being Relation holds
( R is transitive iff for x, y, z being set st [x,y] in R & [y,z] in R holds
[x,z] in R )
Lm3:
for R being Relation holds
( R is antisymmetric iff for x, y being set st [x,y] in R & [y,x] in R holds
x = y )
Lm4:
for R being Relation holds
( R is connected iff for x, y being set st x in field R & y in field R & x <> y & not [x,y] in R holds
[y,x] in R )
Lm5:
for X being set
for R being Relation holds dom (X |` R) c= dom R