let E be set ; :: thesis: for A, B, C being Subset of (E ^omega) st A c= C ? & B c= C ? holds
A ^^ B c= C |^ (0,2)
let A, B, C 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:17;
hence A ^^ B c= C |^ (0,2) by Th93; :: thesis: verum