take bool X ; :: thesis: for F being SetSequence of X st rng F c= bool X holds
Union F in bool X
thus for F being SetSequence of X st rng F c= bool X holds
Union F in bool X ; :: thesis: verum