let A be set ; :: thesis: for u being Element of (NormForm A)

for X being set st X c= u holds

X is Element of (NormForm A)

let u be Element of (NormForm A); :: thesis: for X being set st X c= u holds

X is Element of (NormForm A)

let X be set ; :: thesis: ( X c= u implies X is Element of (NormForm A) )

assume A1: X c= u ; :: thesis: X is Element of (NormForm A)

u = @ u ;

then X in Normal_forms_on A by A1, Th4;

hence X is Element of (NormForm A) by NORMFORM:def 12; :: thesis: verum

for X being set st X c= u holds

X is Element of (NormForm A)

let u be Element of (NormForm A); :: thesis: for X being set st X c= u holds

X is Element of (NormForm A)

let X be set ; :: thesis: ( X c= u implies X is Element of (NormForm A) )

assume A1: X c= u ; :: thesis: X is Element of (NormForm A)

u = @ u ;

then X in Normal_forms_on A by A1, Th4;

hence X is Element of (NormForm A) by NORMFORM:def 12; :: thesis: verum