let X be non empty finite-character set ; :: thesis: for C being c=-linear Subset of X holds union C in X
let C be c=-linear Subset of X; :: thesis: union C in X
set U = union C;
for B being finite Subset of (union C) holds B in X

proof

let B be finite Subset of (union C); :: thesis: B in X

per cases ( C = {} or C <> {} ) ;

suppose C = {} ; :: thesis: B in X

then B = {} by ZFMISC_1:2;
hence B in X by Lm58; :: thesis: verum

end;

suppose C <> {} ; :: thesis: B in X

then consider Z being set such that
A2: ( B c= Z & Z in C ) by PL_AXIOM:16;
thus B in X by A2, Def20r; :: thesis: verum

end;

end;

end;

hence union C in X by Def20r; :: thesis: verum