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