let R be Relation; :: thesis: for X being set st R partially_orders X holds
R |_2 X is Order of X
let X be set ; :: thesis: ( R partially_orders X implies R |_2 X is Order of X )
assume A1: R partially_orders X ; :: thesis: R |_2 X is Order of X
then A2: R is_reflexive_in X by Def7;
set S = R |_2 X;
A3: R |_2 X is_reflexive_in X

proof

let x be set ; :: according to RELAT_2:def 1 :: thesis: ( not x in X or [x,x] in R |_2 X )
assume x in X ; :: thesis: [x,x] in R |_2 X
then ( [x,x] in [:X,X:] & [x,x] in R ) by A2, RELAT_2:def 1, ZFMISC_1:106;
hence [x,x] in R |_2 X by XBOOLE_0:def 4; :: thesis: verum

end;

A4: field (R |_2 X) c= X by WELLORD1:20;
( dom (R |_2 X) c= field (R |_2 X) & rng (R |_2 X) c= field (R |_2 X) ) by XBOOLE_1:7;
then ( dom (R |_2 X) c= X & rng (R |_2 X) c= X ) by A4, XBOOLE_1:1;
then reconsider S = R |_2 X as Relation of X by RELSET_1:11;
A5: dom S = X by A3, Th98;
A6: field S = X by A3, Th98;
A7: R |_2 X is_antisymmetric_in X

proof

let x be set ; :: according to RELAT_2:def 4 :: thesis: for b₁ being set holds
( not x in X or not b₁ in X or not [x,b₁] in R |_2 X or not [b₁,x] in R |_2 X or x = b₁ )
let y be set ; :: thesis: ( not x in X or not y in X or not [x,y] in R |_2 X or not [y,x] in R |_2 X or x = y )
assume that
A8: ( x in X & y in X ) and
A9: ( [x,y] in R |_2 X & [y,x] in R |_2 X ) ; :: thesis: x = y
( [x,y] in R & [y,x] in R & R is_antisymmetric_in X ) by A1, A9, Def7, XBOOLE_0:def 4;
hence x = y by A8, RELAT_2:def 4; :: thesis: verum

end;

R |_2 X is_transitive_in X

proof

let x be set ; :: according to RELAT_2:def 8 :: thesis: for b₁, b₂ being set holds
( not x in X or not b₁ in X or not b₂ in X or not [x,b₁] in R |_2 X or not [b₁,b₂] in R |_2 X or [x,b₂] in R |_2 X )
let y, z be set ; :: thesis: ( not x in X or not y in X or not z in X or not [x,y] in R |_2 X or not [y,z] in R |_2 X or [x,z] in R |_2 X )
assume that
A10: ( x in X & y in X & z in X ) and
A11: ( [x,y] in R |_2 X & [y,z] in R |_2 X ) ; :: thesis: [x,z] in R |_2 X
( [x,y] in R & [y,z] in R & R is_transitive_in X ) by A1, A11, Def7, XBOOLE_0:def 4;
then ( [x,z] in R & [x,z] in [:X,X:] ) by A10, RELAT_2:def 8, ZFMISC_1:106;
hence [x,z] in R |_2 X by XBOOLE_0:def 4; :: thesis: verum

end;

hence R |_2 X is Order of X by A3, A5, A6, A7, PARTFUN1:def 4, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16; :: thesis: verum