union X c= the carrier of L

proof

hence
union X is Subset of L
; :: thesis: verum
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;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