set R = the non empty strict Poset;
take the non empty strict Poset ; :: thesis: ( not the non empty strict Poset is void & not the non empty strict Poset is empty & the non empty strict Poset is strict )
( ex x being object st x in the carrier of the non empty strict Poset & the InternalRel of the non empty strict Poset is_reflexive_in the carrier of the non empty strict Poset ) by ORDERS_2:def 2, XBOOLE_0:def 1;
hence not the InternalRel of the non empty strict Poset is empty ; :: according to YELLOW_3:def 3 :: thesis: ( not the non empty strict Poset is empty & the non empty strict Poset is strict )
thus ( not the non empty strict Poset is empty & the non empty strict Poset is strict ) ; :: thesis: verum