let T be reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure ; :: thesis: for t being type of T
for a being adjective of T
for A, B being Subset of the adjectives of T st B = A \/ {a} & B is_applicable_to t holds
a ast (A ast t) = B ast t
let t be type of T; :: thesis: for a being adjective of T
for A, B being Subset of the adjectives of T st B = A \/ {a} & B is_applicable_to t holds
a ast (A ast t) = B ast t
let a be adjective of T; :: thesis: for A, B being Subset of the adjectives of T st B = A \/ {a} & B is_applicable_to t holds
a ast (A ast t) = B ast t
let A, B be Subset of the adjectives of T; :: thesis: ( B = A \/ {a} & B is_applicable_to t implies a ast (A ast t) = B ast t )
assume A1: ( B = A \/ {a} & B is_applicable_to t ) ; :: thesis: a ast (A ast t) = B ast t
A2: ( A c= B & {a} c= B ) by A1, XBOOLE_1:7;
A3: A is_applicable_to t by A1, Th55, XBOOLE_1:7;
(types a) /\ (downarrow (A ast t)) = (types B) /\ (downarrow t)

proof

thus (types a) /\ (downarrow (A ast t)) c= (types B) /\ (downarrow t) :: according to XBOOLE_0:def 10 :: thesis: (types B) /\ (downarrow t) c= (types a) /\ (downarrow (A ast t))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (types a) /\ (downarrow (A ast t)) or x in (types B) /\ (downarrow t) )
assume A4: x in (types a) /\ (downarrow (A ast t)) ; :: thesis: x in (types B) /\ (downarrow t)
then A5: ( x in types a & x in downarrow (A ast t) ) by XBOOLE_0:def 4;
reconsider t' = x as type of T by A4;
A6: ( t' <= A ast t & A ast t <= t & A c= adjs (A ast t) ) by A3, A5, Th50, Th51, WAYBEL_0:17;
then t' <= t by YELLOW_0:def 2;
then A7: t' in downarrow t by WAYBEL_0:17;
( a in adjs t' & adjs (A ast t) c= adjs t' ) by A5, A6, Th10, Th13;
then ( A c= adjs t' & {a} c= adjs t' ) by A6, XBOOLE_1:1, ZFMISC_1:37;
then B c= adjs t' by A1, XBOOLE_1:8;
then t' in types B by Th14;
hence x in (types B) /\ (downarrow t) by A7, XBOOLE_0:def 4; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (types B) /\ (downarrow t) or x in (types a) /\ (downarrow (A ast t)) )
assume A8: x in (types B) /\ (downarrow t) ; :: thesis: x in (types a) /\ (downarrow (A ast t))
then A9: ( x in types B & x in downarrow t ) by XBOOLE_0:def 4;
reconsider t' = x as type of T by A8;
A10: ( t' <= t & B c= adjs t' & a in B ) by A2, A9, Th14, WAYBEL_0:17, ZFMISC_1:37;
then A c= adjs t' by A2, XBOOLE_1:1;
then ( t' <= A ast t & a in adjs t' ) by A10, Th53;
then ( t' in downarrow (A ast t) & t' in types a ) by Th13, WAYBEL_0:17;
hence x in (types a) /\ (downarrow (A ast t)) by XBOOLE_0:def 4; :: thesis: verum

end;

hence a ast (A ast t) = B ast t ; :: thesis: verum