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

proof

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

end;

the carrier of W is Coset of W by VECTSP_4:73;
then the carrier of W in { A where A is Coset of W : verum } ;
hence { A where A is Coset of W : verum } is non empty Subset-Family of V by A1; :: thesis: verum