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 meets A

let A be Subset of Y; :: thesis: for x being Point of Y st MaxADSet x meets MaxADSet A holds
MaxADSet x meets A

let x be Point of Y; :: thesis: ( MaxADSet x meets MaxADSet A implies MaxADSet x meets A )
set E = { () where a is Point of Y : a in A } ;
assume (MaxADSet x) /\ () <> {} ; :: according to XBOOLE_0:def 7 :: thesis:
then consider z being object such that
A1: z in () /\ () by XBOOLE_0:def 1;
reconsider z = z as Point of Y by A1;
z in MaxADSet A by ;
then consider C being set such that
A2: z in C and
A3: C in { () where a is Point of Y : a in A } by TARSKI:def 4;
z in MaxADSet x by ;
then A4: MaxADSet z = MaxADSet x by Th21;
consider b being Point of Y such that
A5: C = MaxADSet b and
A6: b in A by A3;
MaxADSet b = MaxADSet z by A2, A5, Th21;
then {b} c= MaxADSet x by ;
then b in MaxADSet x by ZFMISC_1:31;
hence MaxADSet x meets A by ; :: thesis: verum