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)
A1: MaxADSet (A \/ B) c= (MaxADSet A) \/ (MaxADSet B)

proof

let x be object ; :: 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 :: thesis: x in (MaxADSet A) \/ (MaxADSet B)

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 :: thesis: ex C being set st
( x in C & C in { (MaxADSet c) where c is Point of Y : c in A } )

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 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: verum

end;

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

now :: thesis: ex C being set st
( x in C & C in { (MaxADSet c) where c is Point of Y : c in B } )

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, A8; :: thesis: verum

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: verum

end;

end;

end;

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

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: verum