let A be set ; :: thesis: for K being Element of Normal_forms_on A
for X being set st X c= K holds
X in Normal_forms_on A
let K be Element of Normal_forms_on A; :: thesis: for X being set st X c= K holds
X in Normal_forms_on A
let X be set ; :: thesis: ( X c= K implies X in Normal_forms_on A )
assume A1: X c= K ; :: thesis: X in Normal_forms_on A
K c= DISJOINT_PAIRS A by FINSUB_1:def 5;
then X c= DISJOINT_PAIRS A by A1, XBOOLE_1:1;
then reconsider B = X as Element of Fin (DISJOINT_PAIRS A) by A1, FINSUB_1:def 5;
for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds
a = b by A1, NORMFORM:32;
hence X in Normal_forms_on A ; :: thesis: verum