let E be set ; :: thesis: for A, B being Subset of E st ( for x being Element of E st x in A holds
x in B ) holds
A c= B
let A, B be Subset of E; :: thesis: ( ( for x being Element of E st x in A holds
x in B ) implies A c= B )
assume A1: for x being Element of E st x in A holds
x in B ; :: thesis: A c= B
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in B )
assume A2: x in A ; :: thesis: x in B
then x in E by Lm1;
then x is Element of E by Def2;
hence x in B by A1, A2; :: thesis: verum