environ
vocabularies HIDDEN, RELAT_1, RELAT_2, XBOOLE_0, SUBSET_1, TARSKI, FUNCT_1, ZFMISC_1, WELLORD1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1;
definitions TARSKI, XBOOLE_0, FUNCT_1, RELAT_1;
theorems TARSKI, XBOOLE_0, FUNCT_1, RELAT_1, RELAT_2, ZFMISC_1, XBOOLE_1, XTUPLE_0;
schemes XBOOLE_0, FUNCT_1;
registrations FUNCT_1, RELAT_1;
constructors HIDDEN, TARSKI, SUBSET_1, FUNCT_1, RELAT_2, XTUPLE_0;
requirements HIDDEN, SUBSET, BOOLE;
equalities TARSKI, XBOOLE_0, RELAT_1;
expansions TARSKI, XBOOLE_0, FUNCT_1;
Lm1:
for R being Relation holds
( R is reflexive iff for x being object st x in field R holds
[x,x] in R )
by RELAT_2:def 1, RELAT_2:def 9;
Lm2:
for R being Relation holds
( R is transitive iff for x, y, z being object 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 object 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 object st x in field R & y in field R & x <> y & not [x,y] in R holds
[y,x] in R )
by RELAT_2:def 6, RELAT_2:def 14;
Lm5:
for X being set
for R being Relation holds dom (X |` R) c= dom R