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

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