set M = { (MaxADSet a) where a is Point of Y : a in A } ;
{ (MaxADSet a) where a is Point of Y : a in A } c= bool the carrier of Y

proof

let C be object ; :: according to TARSKI:def 3 :: thesis: ( not C in { (MaxADSet a) where a is Point of Y : a in A } or C in bool the carrier of Y )
assume C in { (MaxADSet a) where a is Point of Y : a in A } ; :: thesis: C in bool the carrier of Y
then ex a being Point of Y st
( C = MaxADSet a & a in A ) ;
hence C in bool the carrier of Y ; :: thesis: verum

end;

then reconsider M = { (MaxADSet a) where a is Point of Y : a in A } as Subset-Family of Y ;
union M is Subset of Y ;
hence union { (MaxADSet a) where a is Point of Y : a in A } is Subset of Y ; :: thesis: verum