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)

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

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

A10:
MaxADSet B c= MaxADSet (A \/ B)
by Th31, XBOOLE_1:7;
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;

end;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)end;

hence
x in (MaxADSet A) \/ (MaxADSet B)
; :: thesis: verumper cases
( a in A or a in B )
by A5, XBOOLE_0:def 3;

end;

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

MaxADSet A c= (MaxADSet A) \/ (MaxADSet B) by XBOOLE_1:7;

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

end;

now :: thesis: ex C being set st

( x in C & C in { (MaxADSet c) where c is Point of Y : c in A } )

then A7:
x in MaxADSet A
by TARSKI:def 4;( 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;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

MaxADSet A c= (MaxADSet A) \/ (MaxADSet B) by XBOOLE_1:7;

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

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

MaxADSet B c= (MaxADSet A) \/ (MaxADSet B) by XBOOLE_1:7;

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

end;

now :: thesis: ex C being set st

( x in C & C in { (MaxADSet c) where c is Point of Y : c in B } )

then A9:
x in MaxADSet B
by TARSKI:def 4;( 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;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

MaxADSet B c= (MaxADSet A) \/ (MaxADSet B) by XBOOLE_1:7;

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

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