let A be non empty set ; :: thesis: 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_fun (d,q) is symmetric
let L be lower-bounded LATTICE; :: thesis: 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_fun (d,q) is symmetric
let d be BiFunction of A,L; :: thesis: ( d is symmetric implies for q being Element of [:A,A, the carrier of L, the carrier of L:] holds new_bi_fun (d,q) is symmetric )
assume A1: d is symmetric ; :: thesis: for q being Element of [:A,A, the carrier of L, the carrier of L:] holds new_bi_fun (d,q) is symmetric
let q be Element of [:A,A, the carrier of L, the carrier of L:]; :: thesis: new_bi_fun (d,q) is symmetric
set f = new_bi_fun (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_set A; :: according to LATTICE5:def 5 :: thesis: (new_bi_fun (d,q)) . (p,q) = (new_bi_fun (d,q)) . (q,p)
A2: ( p in A or p in {{A},{{A}},{{{A}}}} ) by XBOOLE_0:def 3;
A3: ( q in A or q in {{A},{{A}},{{{A}}}} ) by XBOOLE_0:def 3;