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)
A1: MaxADSet (A /\ B) c= MaxADSet B by Th31, XBOOLE_1:17;
MaxADSet (A /\ B) c= MaxADSet A by Th31, XBOOLE_1:17;
hence MaxADSet (A /\ B) c= (MaxADSet A) /\ (MaxADSet B) by A1, XBOOLE_1:19; :: thesis: verum