( ( for x being Element of L st x in A holds
x in B ) implies A c= B )

proof

assume A1: for x being Element of L st x in A holds
x in B ; :: thesis: A c= B
thus A c= B :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in B )
assume x in A ; :: thesis: x in B
hence x in B by A1; :: thesis: verum

end;

end;

hence ( A c= B iff for x being Element of L st x in A holds
x in B ) ; :: thesis: verum