let Y be non empty TopStruct ; :: thesis:
let A, B be Subset of Y; :: thesis:
set E = { (MaxADSet a) where a is Point of Y : a in A } ;
set F = { (MaxADSet b) where b is Point of Y : b in B } ;
assume A1: A c= B ; :: thesis:
{ (MaxADSet a) where a is Point of Y : a in A } c= { (MaxADSet b) where b is Point of Y : b in B }

let C be object ; :: according to TARSKI:def 3 :: thesis:
assume C in { (MaxADSet a) where a is Point of Y : a in A } ; :: thesis:
then ex a being Point of Y st
( C = MaxADSet a & a in A ) ;
hence C in { (MaxADSet b) where b is Point of Y : b in B } by A1; :: thesis:

end;