set X = LTLnode(# ({} v),({} v),({} v) #);
take LTLnode(# ({} v),({} v),({} v) #) ; :: thesis: ( LTLnode(# ({} v),({} v),({} v) #) is elementary & LTLnode(# ({} v),({} v),({} v) #) is strict )
thus ( LTLnode(# ({} v),({} v),({} v) #) is elementary & LTLnode(# ({} v),({} v),({} v) #) is strict ) by Defelementary; :: thesis: verum