let Y be non empty TopStruct ; :: thesis: for A, B being Subset of Y holds MaxADSet (A \/ B) = (MaxADSet A) \/ (MaxADSet B)
let A, B be Subset of Y; :: thesis: MaxADSet (A \/ B) = (MaxADSet A) \/ (MaxADSet B)
( MaxADSet A c= MaxADSet (A \/ B) & MaxADSet B c= MaxADSet (A \/ B) ) by Th33, XBOOLE_1:7;
then A1: (MaxADSet A) \/ (MaxADSet B) c= MaxADSet (A \/ B) by XBOOLE_1:8;
MaxADSet (A \/ B) c= (MaxADSet A) \/ (MaxADSet B)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in MaxADSet (A \/ B) or x in (MaxADSet A) \/ (MaxADSet B) )
assume x in MaxADSet (A \/ B) ; :: thesis: x in (MaxADSet A) \/ (MaxADSet B)
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

per cases ( a in A or a in B ) by A5, XBOOLE_0:def 3;

suppose A6: a in A ; :: thesis: x in (MaxADSet A) \/ (MaxADSet B)

now

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

end;

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

end;

suppose A7: a in B ; :: thesis: x in (MaxADSet A) \/ (MaxADSet B)

now

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

end;

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

end;

end;

end;

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

end;

hence MaxADSet (A \/ B) = (MaxADSet A) \/ (MaxADSet B) by A1, XBOOLE_0:def 10; :: thesis: verum