let A be set ; :: thesis: for u being Element of
for X being set st X c= u holds
X is Element of
let u be Element of ; :: thesis: for X being set st X c= u holds
X is Element of
let X be set ; :: thesis: ( X c= u implies X is Element of )
assume A1: X c= u ; :: thesis: X is Element of
u = @ u ;
then X in Normal_forms_on A by A1, Th8;
hence X is Element of by NORMFORM:def 14; :: thesis: verum