let R be Relation; for Y, X being set st R linearly_orders Y & X c= Y holds
R linearly_orders X
let Y, X be set ; ( R linearly_orders Y & X c= Y implies R linearly_orders X )
assume that
A1:
R is_reflexive_in Y
and
A2:
R is_transitive_in Y
and
A3:
R is_antisymmetric_in Y
and
A4:
R is_connected_in Y
and
A5:
X c= Y
; ORDERS_1:def 8 R linearly_orders X
thus
( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X & R is_connected_in X )
by A1, A2, A3, A4, A5, Lm10, Th93, Th94, Th95; ORDERS_1:def 8 verum