let R be Relation; for X being set st R is being_linear-order holds
R |_2 X is being_linear-order
let X be set ; ( R is being_linear-order implies R |_2 X is being_linear-order )
assume that
A1:
R is reflexive
and
A2:
R is transitive
and
A3:
R is antisymmetric
and
A4:
R is connected
; ORDERS_1:def 5 R |_2 X is being_linear-order
thus
( R |_2 X is reflexive & R |_2 X is transitive & R |_2 X is antisymmetric & R |_2 X is connected )
by A1, A2, A3, A4, WELLORD1:22, WELLORD1:23, WELLORD1:24, WELLORD1:25; ORDERS_1:def 5 verum