let A be non empty set ; for L being lower-bounded LATTICE
for d being BiFunction of A,L st d is symmetric holds
for q being Element of [:A,A, the carrier of L, the carrier of L:] holds new_bi_fun2 (d,q) is symmetric
let L be lower-bounded LATTICE; for d being BiFunction of A,L st d is symmetric holds
for q being Element of [:A,A, the carrier of L, the carrier of L:] holds new_bi_fun2 (d,q) is symmetric
let d be BiFunction of A,L; ( d is symmetric implies for q being Element of [:A,A, the carrier of L, the carrier of L:] holds new_bi_fun2 (d,q) is symmetric )
assume A1:
d is symmetric
; for q being Element of [:A,A, the carrier of L, the carrier of L:] holds new_bi_fun2 (d,q) is symmetric
let q be Element of [:A,A, the carrier of L, the carrier of L:]; new_bi_fun2 (d,q) is symmetric
set f = new_bi_fun2 (d,q);
set x = q `1_4 ;
set y = q `2_4 ;
set a = q `3_4 ;
set b = q `4_4 ;
let p, q be Element of new_set2 A; LATTICE5:def 5 (new_bi_fun2 (d,q)) . (p,q) = (new_bi_fun2 (d,q)) . (q,p)
A2:
( p in A or p in {{A},{{A}}} )
by XBOOLE_0:def 3;
A3:
( q in A or q in {{A},{{A}}} )
by XBOOLE_0:def 3;