let X be non empty set ; :: thesis: for x, y being set st x c= y holds
{ t where t is Element of X : y c= t } c= { z where z is Element of X : x c= z }
let x, y be set ; :: thesis: ( x c= y implies { t where t is Element of X : y c= t } c= { z where z is Element of X : x c= z } )
assume A1: x c= y ; :: thesis: { t where t is Element of X : y c= t } c= { z where z is Element of X : x c= z }
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { t where t is Element of X : y c= t } or a in { z where z is Element of X : x c= z } )
assume a in { t where t is Element of X : y c= t } ; :: thesis: a in { z where z is Element of X : x c= z }
then consider b being Element of X such that
A2: ( b = a & y c= b ) ;
x c= a by A1, A2, XBOOLE_1:1;
hence a in { z where z is Element of X : x c= z } by A2; :: thesis: verum