set C = { A where A is Coset of Y : verum } ;
A1: { A where A is Coset of Y : verum } c= bool the carrier of X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { A where A is Coset of Y : verum } or x in bool the carrier of X )
assume x in { A where A is Coset of Y : verum } ; :: thesis: x in bool the carrier of X
then ex A being Coset of Y st A = x ;
hence x in bool the carrier of X ; :: thesis: verum

end;

the carrier of Y is Coset of Y by RLSUB_1:74;
then the carrier of Y in { A where A is Coset of Y : verum } ;
hence { A where A is Coset of Y : verum } is non empty Subset-Family of X by A1; :: thesis: verum