set x = the Element of T;
take { the Element of T} opp+id ; :: thesis: ( { the Element of T} opp+id is monotone & { the Element of T} opp+id is antitone & { the Element of T} opp+id is reflexive & { the Element of T} opp+id is strict )
thus ( { the Element of T} opp+id is monotone & { the Element of T} opp+id is antitone & { the Element of T} opp+id is reflexive & { the Element of T} opp+id is strict ) ; :: thesis: verum