let Y be non empty TopStruct ; :: thesis:
let A, B be Subset of Y; :: thesis:
A1: MaxADSet (A \/ B) c= (MaxADSet A) \/ (MaxADSet B)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in MaxADSet (A \/ B) ; :: thesis:
then consider C being set such that
A2: x in C and
A3: C in { (MaxADSet a) where a is Point of Y : a in A \/ B } by TARSKI:def 4;
consider a being Point of Y such that
A4: C = MaxADSet a and
A5: a in A \/ B by A3;

now :: thesis:

per cases by A5, XBOOLE_0:def 3;

suppose A6: a in A ; :: thesis:

now :: thesis:

take C = C; :: thesis:
thus x in C by A2; :: thesis:
thus C in { (MaxADSet c) where c is Point of Y : c in A } by A4, A6; :: thesis:

end;

then A7: x in MaxADSet A by TARSKI:def 4;
MaxADSet A c= (MaxADSet A) \/ (MaxADSet B) by XBOOLE_1:7;
hence x in (MaxADSet A) \/ (MaxADSet B) by A7; :: thesis:

end;

suppose A8: a in B ; :: thesis:

now :: thesis:

take C = C; :: thesis:
thus x in C by A2; :: thesis:
thus C in { (MaxADSet c) where c is Point of Y : c in B } by A4, A8; :: thesis:

end;

then A9: x in MaxADSet B by TARSKI:def 4;
MaxADSet B c= (MaxADSet A) \/ (MaxADSet B) by XBOOLE_1:7;
hence x in (MaxADSet A) \/ (MaxADSet B) by A9; :: thesis:

end;

end;

end;

hence x in (MaxADSet A) \/ (MaxADSet B) ; :: thesis:

end;

A10: MaxADSet B c= MaxADSet (A \/ B) by Th31, XBOOLE_1:7;
MaxADSet A c= MaxADSet (A \/ B) by Th31, XBOOLE_1:7;
then (MaxADSet A) \/ (MaxADSet B) c= MaxADSet (A \/ B) by A10, XBOOLE_1:8;
hence MaxADSet (A \/ B) = (MaxADSet A) \/ (MaxADSet B) by A1; :: thesis: