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