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