let Y be non empty TopStruct ; :: thesis: for A, B being Subset of Y holds MaxADSet (A \/ B) = () \/ ()
let A, B be Subset of Y; :: thesis: MaxADSet (A \/ B) = () \/ ()
A1: MaxADSet (A \/ B) c= () \/ ()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in MaxADSet (A \/ B) or x in () \/ () )
assume x in MaxADSet (A \/ B) ; :: thesis: x in () \/ ()
then consider C being set such that
A2: x in C and
A3: C in { () 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 () \/ ()
per cases ( a in A or a in B ) by ;
suppose A6: a in A ; :: thesis: x in () \/ ()
now :: thesis: ex C being set st
( x in C & C in { () where c is Point of Y : c in A } )
take C = C; :: thesis: ( x in C & C in { () where c is Point of Y : c in A } )
thus x in C by A2; :: thesis: C in { () where c is Point of Y : c in A }
thus C in { () 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= () \/ () by XBOOLE_1:7;
hence x in () \/ () by A7; :: thesis: verum
end;
suppose A8: a in B ; :: thesis: x in () \/ ()
now :: thesis: ex C being set st
( x in C & C in { () where c is Point of Y : c in B } )
take C = C; :: thesis: ( x in C & C in { () where c is Point of Y : c in B } )
thus x in C by A2; :: thesis: C in { () where c is Point of Y : c in B }
thus C in { () 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= () \/ () by XBOOLE_1:7;
hence x in () \/ () by A9; :: thesis: verum
end;
end;
end;
hence x in () \/ () ; :: thesis: verum
end;