set A = the non empty set ;
take PrefSpace the non empty set ; :: thesis: ( not PrefSpace the non empty set is empty & PrefSpace the non empty set is strict & PrefSpace the non empty set is preference-like )
thus ( not PrefSpace the non empty set is empty & PrefSpace the non empty set is strict & PrefSpace the non empty set is preference-like ) ; :: thesis: verum