set A = the non empty set ;
set R = the Relation of [: the non empty set , the non empty set :];
take AffinStruct(# the non empty set , the Relation of [: the non empty set , the non empty set :] #) ; :: thesis: ( not AffinStruct(# the non empty set , the Relation of [: the non empty set , the non empty set :] #) is empty & AffinStruct(# the non empty set , the Relation of [: the non empty set , the non empty set :] #) is strict )
thus not the carrier of AffinStruct(# the non empty set , the Relation of [: the non empty set , the non empty set :] #) is empty ; :: according to STRUCT_0:def 1 :: thesis: AffinStruct(# the non empty set , the Relation of [: the non empty set , the non empty set :] #) is strict
thus AffinStruct(# the non empty set , the Relation of [: the non empty set , the non empty set :] #) is strict ; :: thesis: verum