let E be set ; :: thesis: for A, B being Subset of (E ^omega) holds (A /\ B) ? = (A ?) /\ (B ?)
let A, B be Subset of (E ^omega); :: thesis: (A /\ B) ? = (A ?) /\ (B ?)
thus (A /\ B) ? = {(<%> E)} \/ (A /\ B) by Th76
.= ({(<%> E)} \/ A) /\ ({(<%> E)} \/ B) by XBOOLE_1:24
.= (A ?) /\ ({(<%> E)} \/ B) by Th76
.= (A ?) /\ (B ?) by Th76 ; :: thesis: verum