let x, X be set ; :: thesis: ( X is c=-linear implies X \/ {((union X) \/ x)} is c=-linear )
assume A1: X is c=-linear ; :: thesis: X \/ {((union X) \/ x)} is c=-linear
set U = union X;
set Ux = (union X) \/ x;
A2: union X c= (union X) \/ x by XBOOLE_1:7;
let x1, x2 be set ; :: according to ORDINAL1:def 8 :: thesis: ( not x1 in X \/ {((union X) \/ x)} or not x2 in X \/ {((union X) \/ x)} or x1,x2 are_c=-comparable )
assume A3: ( x1 in X \/ {((union X) \/ x)} & x2 in X \/ {((union X) \/ x)} ) ; :: thesis: x1,x2 are_c=-comparable

per cases ( ( x1 in X & x2 in X ) or ( x1 in {((union X) \/ x)} & x2 in {((union X) \/ x)} ) or ( x1 in X & x2 in {((union X) \/ x)} ) or ( x2 in X & x1 in {((union X) \/ x)} ) ) by A3, XBOOLE_0:def 3;

suppose ( x1 in X & x2 in X ) ; :: thesis: x1,x2 are_c=-comparable

hence x1,x2 are_c=-comparable by A1; :: thesis: verum

end;

suppose A4: ( x1 in {((union X) \/ x)} & x2 in {((union X) \/ x)} ) ; :: thesis: x1,x2 are_c=-comparable

then x1 = (union X) \/ x by TARSKI:def 1;
hence x1,x2 are_c=-comparable by A4, TARSKI:def 1; :: thesis: verum

end;

suppose ( x1 in X & x2 in {((union X) \/ x)} ) ; :: thesis: x1,x2 are_c=-comparable

then ( x1 c= union X & x2 = (union X) \/ x ) by TARSKI:def 1, ZFMISC_1:74;
then x1 c= x2 by A2;
hence x1,x2 are_c=-comparable ; :: thesis: verum

end;

suppose ( x2 in X & x1 in {((union X) \/ x)} ) ; :: thesis: x1,x2 are_c=-comparable

then ( x2 c= union X & x1 = (union X) \/ x ) by TARSKI:def 1, ZFMISC_1:74;
then x2 c= x1 by A2;
hence x1,x2 are_c=-comparable ; :: thesis: verum

end;

end;