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

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

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

proof

then reconsider M = { (MaxADSet a) where a is Point of Y : a in A } as Subset-Family of Y ;
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;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

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