[#] Y = the carrier of Y ;
then reconsider A0 = the carrier of Y as non empty Subset of Y ;
set Y0 = Y | A0;
take Y | A0 ; :: thesis: ( not Y | A0 is proper & Y | A0 is strict )
A0 = [#] (Y | A0) by PRE_TOPC:def 5;
hence ( not Y | A0 is proper & Y | A0 is strict ) by TEX_2:10; :: thesis: verum