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