set LCS = { (x * N) where x is Element of Q : verum } ;
{ (x * N) where x is Element of Q : verum } c= bool the carrier of Q

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (x * N) where x is Element of Q : verum } or x in bool the carrier of Q )
assume x in { (x * N) where x is Element of Q : verum } ; :: thesis: x in bool the carrier of Q
then ex y being Element of Q st x = y * N ;
hence x in bool the carrier of Q ; :: thesis: verum

end;

then reconsider LCS = { (x * N) where x is Element of Q : verum } as Subset-Family of Q ;
take LCS ; :: thesis: for H being Subset of Q holds
( H in LCS iff ex x being Element of Q st H = x * N )
thus for H being Subset of Q holds
( H in LCS iff ex x being Element of Q st H = x * N ) ; :: thesis: verum