let R be Relation; :: thesis: ( {} * R = {} & R * {} = {} )

A1: now

let x, y be set ; :: thesis: ( [x,y] in {} * R iff [x,y] in {} )

now

assume [x,y] in {} * R ; :: thesis: ( {} * R = {} & R * {} = {} )
then ex z being set st
( [x,z] in {} & [z,y] in R ) by Def8;
hence ( {} * R = {} & R * {} = {} ) ; :: thesis: verum

end;

hence ( [x,y] in {} * R iff [x,y] in {} ) ; :: thesis: verum

end;

now

let x, y be set ; :: thesis: ( [x,y] in R * {} iff [x,y] in {} )

now

assume [x,y] in R * {} ; :: thesis: ( {} * R = {} & R * {} = {} )
then ex z being set st
( [x,z] in R & [z,y] in {} ) by Def8;
hence ( {} * R = {} & R * {} = {} ) ; :: thesis: verum

end;

hence ( [x,y] in R * {} iff [x,y] in {} ) ; :: thesis: verum

end;

hence ( {} * R = {} & R * {} = {} ) by A1, Def2; :: thesis: verum