set A = the non trivial set ;
set R = the Relation of [: the non trivial set , the non trivial set :];
take AffinStruct(# the non trivial set , the Relation of [: the non trivial set , the non trivial set :] #) ; :: thesis: ( not AffinStruct(# the non trivial set , the Relation of [: the non trivial set , the non trivial set :] #) is trivial & AffinStruct(# the non trivial set , the Relation of [: the non trivial set , the non trivial set :] #) is strict )
thus ( not AffinStruct(# the non trivial set , the Relation of [: the non trivial set , the non trivial set :] #) is trivial & AffinStruct(# the non trivial set , the Relation of [: the non trivial set , the non trivial set :] #) is strict ) ; :: thesis: verum