let X be set ; :: thesis: ( not X is empty & X is finite & X is c=-linear implies union X in X )
assume ( not X is empty & X is finite & X is c=-linear ) ; :: thesis: union X in X
then consider U being set such that
A1: U in X and
A2: for x being set st x in X holds
x c= U by FINSET_1:12;
A3: union X c= U

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union X or x in U )
assume x in union X ; :: thesis: x in U
then consider y being set such that
A4: x in y and
A5: y in X by TARSKI:def 4;
y c= U by A2, A5;
hence x in U by A4; :: thesis: verum

end;

U c= union X by A1, ZFMISC_1:74;
hence union X in X by A1, A3, XBOOLE_0:def 10; :: thesis: verum