let T be non empty reflexive transitive non void TAS-structure ; :: thesis: for t being type of T
for A being Subset of the adjectives of T st A is_properly_applicable_to t holds
ex B being Subset of the adjectives of T st
( B c= A & B is_properly_applicable_to t & A ast t = B ast t & ( for C being Subset of the adjectives of T st C c= B & C is_properly_applicable_to t & A ast t = C ast t holds
C = B ) )
let t be type of T; :: thesis: for A being Subset of the adjectives of T st A is_properly_applicable_to t holds
ex B being Subset of the adjectives of T st
( B c= A & B is_properly_applicable_to t & A ast t = B ast t & ( for C being Subset of the adjectives of T st C c= B & C is_properly_applicable_to t & A ast t = C ast t holds
C = B ) )
let A be Subset of the adjectives of T; :: thesis: ( A is_properly_applicable_to t implies ex B being Subset of the adjectives of T st
( B c= A & B is_properly_applicable_to t & A ast t = B ast t & ( for C being Subset of the adjectives of T st C c= B & C is_properly_applicable_to t & A ast t = C ast t holds
C = B ) ) )
defpred S₁[ set ] means ex B being Subset of the adjectives of T st
( $1 = B & $1 c= A & B is_properly_applicable_to t & A ast t = B ast t );
assume A1: A is_properly_applicable_to t ; :: thesis: ex B being Subset of the adjectives of T st
( B c= A & B is_properly_applicable_to t & A ast t = B ast t & ( for C being Subset of the adjectives of T st C c= B & C is_properly_applicable_to t & A ast t = C ast t holds
C = B ) )
A2: ex a being finite set st S₁[a] by A1;
consider B being finite set such that
A3: S₁[B] and
A4: for C being set st C c= B & S₁[C] holds
C = B from ABCMIZ_0:sch 1(A2);
reconsider B = B as Subset of the adjectives of T by A3;
take B ; :: thesis: ( B c= A & B is_properly_applicable_to t & A ast t = B ast t & ( for C being Subset of the adjectives of T st C c= B & C is_properly_applicable_to t & A ast t = C ast t holds
C = B ) )
thus ( B c= A & B is_properly_applicable_to t & A ast t = B ast t ) by A3; :: thesis: for C being Subset of the adjectives of T st C c= B & C is_properly_applicable_to t & A ast t = C ast t holds
C = B
let C be Subset of the adjectives of T; :: thesis: ( C c= B & C is_properly_applicable_to t & A ast t = C ast t implies C = B )
assume A5: C c= B ; :: thesis: ( not C is_properly_applicable_to t or not A ast t = C ast t or C = B )
then C c= A by A3, XBOOLE_1:1;
hence ( not C is_properly_applicable_to t or not A ast t = C ast t or C = B ) by A4, A5; :: thesis: verum