let OAS be OAffinSpace; :: thesis: for x being set holds
( ( x is Element of implies x is Element of ) & ( x is Element of implies x is Element of ) & ( x is Subset of implies x is Subset of ) & ( x is Subset of implies x is Subset of ) )
Lambda OAS = AffinStruct(# the carrier of OAS,(lambda the CONGR of OAS) #) by DIRAF:def 2;
hence for x being set holds
( ( x is Element of implies x is Element of ) & ( x is Element of implies x is Element of ) & ( x is Subset of implies x is Subset of ) & ( x is Subset of implies x is Subset of ) ) ; :: thesis: verum