let R, P be Relation; :: thesis: ( R misses P & P is symmetric implies R ~ misses P )
assume R misses P ; :: thesis: ( not P is symmetric or R ~ misses P )
then A0: R ~ misses P ~ by LemmaAuxIrr;
assume P is symmetric ; :: thesis: R ~ misses P
hence R ~ misses P by A0, RELAT_2:13; :: thesis: verum