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