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

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

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

proof

the carrier of Y is Coset of Y
by RLSUB_1:74;
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;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

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