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_fun2 (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_fun2 (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_fun2 (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_fun2 (d,q) is symmetric
let q be Element of [:A,A, the carrier of L, the carrier of L:]; :: thesis: 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; :: according to LATTICE5:def 5 :: thesis: (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;

per cases ( ( p in A & q in A ) or ( p in A & q = {A} ) or ( p in A & q = {{A}} ) or ( p = {A} & q in A ) or ( p = {A} & q = {A} ) or ( p = {A} & q = {{A}} ) or ( p = {{A}} & q in A ) or ( p = {{A}} & q = {A} ) or ( p = {{A}} & q = {{A}} ) ) by A2, A3, TARSKI:def 2;

suppose ( p in A & q in A ) ; :: thesis: (new_bi_fun2 (d,q)) . (p,q) = (new_bi_fun2 (d,q)) . (q,p)

then reconsider p9 = p, q9 = q as Element of A ;
thus (new_bi_fun2 (d,q)) . (p,q) = d . (p9,q9) by Def4
.= d . (q9,p9) by A1
.= (new_bi_fun2 (d,q)) . (q,p) by Def4 ; :: thesis: verum

end;

suppose A4: ( p in A & q = {A} ) ; :: thesis: (new_bi_fun2 (d,q)) . (p,q) = (new_bi_fun2 (d,q)) . (q,p)

then reconsider p9 = p as Element of A ;
thus (new_bi_fun2 (d,q)) . (p,q) = (d . (p9,(q `1_4))) "\/" (q `3_4) by A4, Def4
.= (new_bi_fun2 (d,q)) . (q,p) by A4, Def4 ; :: thesis: verum

end;

suppose A5: ( p in A & q = {{A}} ) ; :: thesis: (new_bi_fun2 (d,q)) . (p,q) = (new_bi_fun2 (d,q)) . (q,p)

then reconsider p9 = p as Element of A ;
thus (new_bi_fun2 (d,q)) . (p,q) = (d . (p9,(q `2_4))) "\/" (q `3_4) by A5, Def4
.= (new_bi_fun2 (d,q)) . (q,p) by A5, Def4 ; :: thesis: verum

end;

suppose A6: ( p = {A} & q in A ) ; :: thesis: (new_bi_fun2 (d,q)) . (p,q) = (new_bi_fun2 (d,q)) . (q,p)

then reconsider q9 = q as Element of A ;
thus (new_bi_fun2 (d,q)) . (p,q) = (d . (q9,(q `1_4))) "\/" (q `3_4) by A6, Def4
.= (new_bi_fun2 (d,q)) . (q,p) by A6, Def4 ; :: thesis: verum

end;

suppose ( p = {A} & q = {A} ) ; :: thesis: (new_bi_fun2 (d,q)) . (p,q) = (new_bi_fun2 (d,q)) . (q,p)

hence (new_bi_fun2 (d,q)) . (p,q) = (new_bi_fun2 (d,q)) . (q,p) ; :: thesis: verum

end;

suppose A7: ( p = {A} & q = {{A}} ) ; :: thesis: (new_bi_fun2 (d,q)) . (p,q) = (new_bi_fun2 (d,q)) . (q,p)

hence (new_bi_fun2 (d,q)) . (p,q) = ((d . ((q `1_4),(q `2_4))) "\/" (q `3_4)) "/\" (q `4_4) by Def4
.= (new_bi_fun2 (d,q)) . (q,p) by A7, Def4 ;
:: thesis: verum

end;

suppose A8: ( p = {{A}} & q in A ) ; :: thesis: (new_bi_fun2 (d,q)) . (p,q) = (new_bi_fun2 (d,q)) . (q,p)

then reconsider q9 = q as Element of A ;
thus (new_bi_fun2 (d,q)) . (p,q) = (d . (q9,(q `2_4))) "\/" (q `3_4) by A8, Def4
.= (new_bi_fun2 (d,q)) . (q,p) by A8, Def4 ; :: thesis: verum

end;

suppose A9: ( p = {{A}} & q = {A} ) ; :: thesis: (new_bi_fun2 (d,q)) . (p,q) = (new_bi_fun2 (d,q)) . (q,p)

hence (new_bi_fun2 (d,q)) . (p,q) = ((d . ((q `1_4),(q `2_4))) "\/" (q `3_4)) "/\" (q `4_4) by Def4
.= (new_bi_fun2 (d,q)) . (q,p) by A9, Def4 ;
:: thesis: verum

end;

suppose ( p = {{A}} & q = {{A}} ) ; :: thesis: (new_bi_fun2 (d,q)) . (p,q) = (new_bi_fun2 (d,q)) . (q,p)

hence (new_bi_fun2 (d,q)) . (p,q) = (new_bi_fun2 (d,q)) . (q,p) ; :: thesis: verum

end;

end;