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 )
for x being set st x in A holds
x in {a} \/ A by XBOOLE_0:def 3;
then A1: A c= {a} \/ A by TARSKI:def 3;
assume R linearly_orders {a} \/ A ; :: thesis: R linearly_orders A
hence R linearly_orders A by A1, ORDERS_1:38; :: thesis: verum