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

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

let x be Point of Y; :: thesis: ( MaxADSet x meets MaxADSet A implies MaxADSet x c= MaxADSet A )
set F = { () where b is Point of Y : b in A } ;
assume MaxADSet x meets MaxADSet A ; :: thesis:
then MaxADSet x meets A by Th29;
then consider z being object such that
A1: z in () /\ A by XBOOLE_0:4;
reconsider z = z as Point of Y by A1;
set E = { () where a is Point of Y : a in {z} } ;
z in A by ;
then A2: {z} c= A by ZFMISC_1:31;
{ (MaxADSet a) where a is Point of Y : a in {z} } c= { () where b is Point of Y : b in A }
proof
let C be object ; :: according to TARSKI:def 3 :: thesis: ( not C in { () where a is Point of Y : a in {z} } or C in { () where b is Point of Y : b in A } )
assume C in { () where a is Point of Y : a in {z} } ; :: thesis: C in { () 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 { () 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 ;
hence MaxADSet x c= MaxADSet A by ; :: thesis: verum