let E be set ; :: thesis: for A, C, B being Subset of (E ^omega ) st A c= C ? & B c= C ? holds
A ^^ B c= C |^ 0 ,2
let A, C, B be Subset of (E ^omega ); :: thesis: ( A c= C ? & B c= C ? implies A ^^ B c= C |^ 0 ,2 )
assume ( A c= C ? & B c= C ? ) ; :: thesis: A ^^ B c= C |^ 0 ,2
then A ^^ B c= (C ? ) ^^ (C ? ) by FLANG_1:18;
hence A ^^ B c= C |^ 0 ,2 by Th93; :: thesis: verum