let X be set ; for A being Subset of X
for O being Order of X holds
( O is_reflexive_in A & O is_antisymmetric_in A & O is_transitive_in A )
let A be Subset of X; for O being Order of X holds
( O is_reflexive_in A & O is_antisymmetric_in A & O is_transitive_in A )
let O be Order of X; ( O is_reflexive_in A & O is_antisymmetric_in A & O is_transitive_in A )
A1:
field O = X
by ORDERS_1:12;
then
O is_antisymmetric_in X
by RELAT_2:def 12;
then A2:
for x, y being object st x in A & y in A & [x,y] in O & [y,x] in O holds
x = y
by RELAT_2:def 4;
O is_transitive_in X
by A1, RELAT_2:def 16;
then A3:
for x, y, z being object st x in A & y in A & z in A & [x,y] in O & [y,z] in O holds
[x,z] in O
by RELAT_2:def 8;
O is_reflexive_in X
by A1, RELAT_2:def 9;
then
for x being object st x in A holds
[x,x] in O
by RELAT_2:def 1;
hence
( O is_reflexive_in A & O is_antisymmetric_in A & O is_transitive_in A )
by A2, A3, RELAT_2:def 1, RELAT_2:def 4, RELAT_2:def 8; verum