thus ( B c= C implies for a being Element of A st a in B holds
a in C ) ; :: thesis: ( ( for a being Element of A st a in B holds
a in C ) implies B c= C )
assume A1: for a being Element of A st a in B holds
a in C ; :: thesis: B c= C
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in C )
assume A2: x in B ; :: thesis: x in C
then x is Element of A by SETWISEO:9;
hence x in C by A1, A2; :: thesis: verum