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;

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

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;

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