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 set ; :: 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 consider A being Coset of W such that
A2: A = x ;
thus x in bool the carrier of V by A2; :: thesis: verum

end;

the carrier of W is Coset of W by VECTSP_4:89;
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