let Y be non empty TopStruct ; :: thesis: for A, B being Subset of Y holds MaxADSet (A /\ B) c= (MaxADSet A) /\ (MaxADSet B)
let A, B be Subset of Y; :: thesis: MaxADSet (A /\ B) c= (MaxADSet A) /\ (MaxADSet B)
( MaxADSet (A /\ B) c= MaxADSet A & MaxADSet (A /\ B) c= MaxADSet B ) by Th33, XBOOLE_1:17;
hence MaxADSet (A /\ B) c= (MaxADSet A) /\ (MaxADSet B) by XBOOLE_1:19; :: thesis: verum