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 ;
set y = q `2 ;
set a = q `3 ;
set b = q `4 ;
let p, q be Element of new_set A; :: according to LATTICE5:def 6 :: 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}}}} ) & ( q in A or q in {{A},{{A}},{{{A}}}} ) )
by XBOOLE_0:def 3;