let X be set ; :: thesis: for A being finite Subset of X
for a being Element of X
for R being Order of X st R linearly_orders {a} \/ A holds
R linearly_orders A
let A be finite Subset of X; :: thesis: for a being Element of X
for R being Order of X st R linearly_orders {a} \/ A holds
R linearly_orders A
let a be Element of X; :: thesis: for R being Order of X st R linearly_orders {a} \/ A holds
R linearly_orders A
let R be Order of X; :: thesis: ( R linearly_orders {a} \/ A implies R linearly_orders A )
assume A1: R linearly_orders {a} \/ A ; :: thesis: R linearly_orders A
for x being set st x in A holds
x in {a} \/ A by XBOOLE_0:def 3;
then A c= {a} \/ A by TARSKI:def 3;
hence R linearly_orders A by A1, ORDERS_1:134; :: thesis: verum