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

( ( 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