let x be Element of P; :: thesis: ( x is Function-like & x is Relation-like )

per cases ( P is empty or not P is empty ) ;

suppose P is empty ; :: thesis: ( x is Function-like & x is Relation-like )

hence ( x is Function-like & x is Relation-like ) by SUBSET_1:def 1; :: thesis: verum

end;

suppose not P is empty ; :: thesis: ( x is Function-like & x is Relation-like )

hence ( x is Function-like & x is Relation-like ) by Def13; :: thesis: verum

end;

end;