let L be non empty RelStr ; :: thesis: for x being Element of [:L,L:] holds (sup_op L) . x = (x `1) "\/" (x `2)

let x be Element of [:L,L:]; :: thesis: (sup_op L) . x = (x `1) "\/" (x `2)

the carrier of [:L,L:] = [: the carrier of L, the carrier of L:] by YELLOW_3:def 2;

then ex a, b being object st

( a in the carrier of L & b in the carrier of L & x = [a,b] ) by ZFMISC_1:def 2;

hence (sup_op L) . x = (sup_op L) . ((x `1),(x `2))

.= (x `1) "\/" (x `2) by Def5 ;

:: thesis: verum

let x be Element of [:L,L:]; :: thesis: (sup_op L) . x = (x `1) "\/" (x `2)

the carrier of [:L,L:] = [: the carrier of L, the carrier of L:] by YELLOW_3:def 2;

then ex a, b being object st

( a in the carrier of L & b in the carrier of L & x = [a,b] ) by ZFMISC_1:def 2;

hence (sup_op L) . x = (sup_op L) . ((x `1),(x `2))

.= (x `1) "\/" (x `2) by Def5 ;

:: thesis: verum