let E be set ; :: thesis: for A, B being Subset of E st ( for a being Element of A holds a in B ) holds
A c= B
let A, B be Subset of E; :: thesis: ( ( for a being Element of A holds a in B ) implies A c= B )
assume A1: for a being Element of A holds a in B ; :: thesis: A c= B
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in A or a in B )
assume A2: a in A ; :: thesis: a in B
reconsider a = a as set by TARSKI:1;
a is Element of A by Def1, A2;
hence a in B by A1; :: thesis: verum