:: deftheorem defines Lambda DIRAF:def 2 :
for S being non empty AffinStruct holds Lambda S = AffinStruct(# the carrier of S,(lambda the CONGR of S) #);