let E be set ; :: thesis: for A, B being Subset of (E ^omega) st <%> E in B holds
( A c= A ^^ B & A c= B ^^ A )
let A, B be Subset of (E ^omega); :: thesis: ( <%> E in B implies ( A c= A ^^ B & A c= B ^^ A ) )
assume A1: <%> E in B ; :: thesis: ( A c= A ^^ B & A c= B ^^ A )
thus A c= A ^^ B :: thesis: A c= B ^^ A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in A ^^ B )
assume A2: x in A ; :: thesis: x in A ^^ B
then reconsider xa = x as Element of E ^omega ;
xa ^ {} in A ^^ B by A1, A2, Def1;
hence x in A ^^ B ; :: thesis: verum

end;

thus A c= B ^^ A :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in B ^^ A )
assume A3: x in A ; :: thesis: x in B ^^ A
then reconsider xa = x as Element of E ^omega ;
{} ^ xa in B ^^ A by A1, A3, Def1;
hence x in B ^^ A ; :: thesis: verum

end;