let OAS be OAffinSpace; :: thesis: for x being set holds
( ( x is Element of OAS implies x is Element of (Lambda OAS) ) & ( x is Element of (Lambda OAS) implies x is Element of OAS ) & ( x is Subset of OAS implies x is Subset of (Lambda OAS) ) & ( x is Subset of (Lambda OAS) implies x is Subset of OAS ) )
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 OAS implies x is Element of (Lambda OAS) ) & ( x is Element of (Lambda OAS) implies x is Element of OAS ) & ( x is Subset of OAS implies x is Subset of (Lambda OAS) ) & ( x is Subset of (Lambda OAS) implies x is Subset of OAS ) ) ; :: thesis: verum