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 set ; :: according to TARSKI:def 3 :: thesis: ( not a in A or a in B )
assume a in A ; :: thesis: a in B
then a is Element of A by Def2;
hence a in B by A1; :: thesis: verum