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)

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

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

proof

then reconsider BB = { B where B is Affine Subset of RLS : A c= B } as Subset-Family of RLS ;
let x be object ; :: 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;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

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