let T be consistent TA-structure ; :: thesis: for a being adjective of T holds types a misses types (non- a)
let a be adjective of T; :: thesis: types a misses types (non- a)
assume types a meets types (non- a) ; :: thesis: contradiction
then consider x being object such that
A1: x in types a and
A2: x in types (non- a) by XBOOLE_0:3;
A3: ex t2 being type of T st
( x = t2 & non- a in adjs t2 ) by A2, Def12;
ex t1 being type of T st
( x = t1 & a in adjs t1 ) by A1, Def12;
hence contradiction by A3, Def9; :: thesis: verum