set BB = { B where B is Affine Subset of RLS : A c= B } ;
{ B where B is Affine Subset of RLS : A c= B } c= bool ([#] RLS)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { B where B is Affine Subset of RLS : A c= B } or x in bool ([#] RLS) )
assume x in { B where B is Affine Subset of RLS : A c= B } ; :: thesis: x in bool ([#] RLS)
then ex B being Affine Subset of RLS st
( x = B & A c= B ) ;
hence x in bool ([#] RLS) ; :: thesis: verum

end;

then reconsider BB = { B where B is Affine Subset of RLS : A c= B } as Subset-Family of RLS ;
meet BB is Subset of RLS ;
hence meet { B where B is Affine Subset of RLS : A c= B } is Subset of RLS ; :: thesis: verum