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 }

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

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

then
MaxADSet {z} c= MaxADSet A
by ZFMISC_1:77;
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;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

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