let R be non empty RelStr ; :: thesis: for a, b being object

for RR being Relation of the carrier of R st [a,b] in RR holds

( a is Element of R & b is Element of R )

let a, b be object ; :: thesis: for RR being Relation of the carrier of R st [a,b] in RR holds

( a is Element of R & b is Element of R )

let RR be Relation of the carrier of R; :: thesis: ( [a,b] in RR implies ( a is Element of R & b is Element of R ) )

assume [a,b] in RR ; :: thesis: ( a is Element of R & b is Element of R )

hence ( a is Element of R & b is Element of R ) by ZFMISC_1:87; :: thesis: verum

for RR being Relation of the carrier of R st [a,b] in RR holds

( a is Element of R & b is Element of R )

let a, b be object ; :: thesis: for RR being Relation of the carrier of R st [a,b] in RR holds

( a is Element of R & b is Element of R )

let RR be Relation of the carrier of R; :: thesis: ( [a,b] in RR implies ( a is Element of R & b is Element of R ) )

assume [a,b] in RR ; :: thesis: ( a is Element of R & b is Element of R )

hence ( a is Element of R & b is Element of R ) by ZFMISC_1:87; :: thesis: verum