let X be set ; :: thesis: 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; :: thesis: 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; :: thesis: ( O is_reflexive_in A & O is_antisymmetric_in A & O is_transitive_in A )
field O = X by ORDERS_1:97;
then A1: ( O is_reflexive_in X & O is_antisymmetric_in X & O is_transitive_in X ) by RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16;
then A2: for x being set st x in A holds
[x,x] in O by RELAT_2:def 1;
A3: for x, y being set st x in A & y in A & [x,y] in O & [y,x] in O holds
x = y by A1, RELAT_2:def 4;
for x, y, z being set st x in A & y in A & z in A & [x,y] in O & [y,z] in O holds
[x,z] in O by A1, RELAT_2:def 8;
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; :: thesis: verum