union X c= the carrier of L

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union X or x in the carrier of L )
assume x in union X ; :: thesis: x in the carrier of L
then consider Y being set such that
A1: x in Y and
A2: Y in X by TARSKI:def 4;
reconsider Y = Y as Ideal of L by A2, YELLOW_2:41;
x in Y by A1;
hence x in the carrier of L ; :: thesis: verum

end;

hence union X is Subset of L ; :: thesis: verum