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

proof

let x be object ; :: according to RELAT_1:def 2 :: thesis: for b being object holds
( [x,b] in {} * R iff [x,b] in {} )
let y be object ; :: thesis: ( [x,y] in {} * R iff [x,y] in {} )

hereby :: thesis: ( [x,y] in {} implies [x,y] in {} * R )

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

end;

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

end;

let x be object ; :: according to RELAT_1:def 2 :: thesis: for b being object holds
( [x,b] in R * {} iff [x,b] in {} )
let y be object ; :: thesis: ( [x,y] in R * {} iff [x,y] in {} )

hereby :: thesis: ( [x,y] in {} implies [x,y] in R * {} )

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

end;

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