let OTS be OrdTrapSpace; :: thesis: for x being set holds
( x is Element of iff x is Element of )
let x be set ; :: thesis: ( x is Element of iff x is Element of )
Lambda OTS = AffinStruct(# the carrier of OTS,(lambda the CONGR of OTS) #) by DIRAF:def 2;
hence ( x is Element of iff x is Element of ) ; :: thesis: verum