X c= X ;
then reconsider Z = X as Subset of X ;
take Z ; :: thesis: for x being set st x in [:Z,Z:] holds
F . x in Z
thus for x being set st x in [:Z,Z:] holds
F . x in Z by Th1; :: thesis: verum