let Y be non empty TopStruct ; :: thesis: for A being Subset of Y
for x being Point of Y st MaxADSet x meets MaxADSet A holds
MaxADSet x c= MaxADSet A
let A be Subset of Y; :: thesis: for x being Point of Y st MaxADSet x meets MaxADSet A holds
MaxADSet x c= MaxADSet A
let x be Point of Y; :: thesis: ( MaxADSet x meets MaxADSet A implies MaxADSet x c= MaxADSet A )
set F = { (MaxADSet b) where b is Point of Y : b in A } ;
assume MaxADSet x meets MaxADSet A ; :: thesis: MaxADSet x c= MaxADSet A
then MaxADSet x meets A by Th29;
then consider z being object such that
A1: z in (MaxADSet x) /\ A by XBOOLE_0:4;
reconsider z = z as Point of Y by A1;
set E = { (MaxADSet a) where a is Point of Y : a in {z} } ;
z in A by A1, XBOOLE_0:def 4;
then A2: {z} c= A by ZFMISC_1:31;
{ (MaxADSet a) where a is Point of Y : a in {z} } c= { (MaxADSet b) where b is Point of Y : b in A }

proof

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

end;

then MaxADSet {z} c= MaxADSet A by ZFMISC_1:77;
then A3: MaxADSet z c= MaxADSet A by Th28;
z in MaxADSet x by A1, XBOOLE_0:def 4;
hence MaxADSet x c= MaxADSet A by A3, Th21; :: thesis: verum