let BL be non trivial B_Lattice; :: thesis: for a, b being Element of BL holds (UFilter BL) . (a "\/" b) = ((UFilter BL) . a) \/ ((UFilter BL) . b)
let a, b be Element of BL; :: thesis: (UFilter BL) . (a "\/" b) = ((UFilter BL) . a) \/ ((UFilter BL) . b)
A1: (UFilter BL) . (a "\/" b) c= ((UFilter BL) . a) \/ ((UFilter BL) . b)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (UFilter BL) . (a "\/" b) or x in ((UFilter BL) . a) \/ ((UFilter BL) . b) )
set c = a "\/" b;
assume x in (UFilter BL) . (a "\/" b) ; :: thesis: x in ((UFilter BL) . a) \/ ((UFilter BL) . b)
then consider F0 being Filter of BL such that
A2: x = F0 and
A3: F0 is being_ultrafilter and
A4: a "\/" b in F0 by Th17;
( a in F0 or b in F0 ) by A3, A4, Th19;
then ( F0 in (UFilter BL) . a or F0 in (UFilter BL) . b ) by A3, Th17;
hence x in ((UFilter BL) . a) \/ ((UFilter BL) . b) by A2, XBOOLE_0:def 3; :: thesis: verum

end;

((UFilter BL) . a) \/ ((UFilter BL) . b) c= (UFilter BL) . (a "\/" b)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((UFilter BL) . a) \/ ((UFilter BL) . b) or x in (UFilter BL) . (a "\/" b) )
assume x in ((UFilter BL) . a) \/ ((UFilter BL) . b) ; :: thesis: x in (UFilter BL) . (a "\/" b)
then ( x in (UFilter BL) . a or x in (UFilter BL) . b ) by XBOOLE_0:def 3;
then ( ex F0 being Filter of BL st
( x = F0 & F0 is being_ultrafilter & a in F0 ) or ex F0 being Filter of BL st
( x = F0 & F0 is being_ultrafilter & b in F0 ) ) by Th17;
then consider F0 being Filter of BL such that
A5: x = F0 and
A6: F0 is being_ultrafilter and
A7: ( a in F0 or b in F0 ) ;
a "\/" b in F0 by A6, A7, Th19;
hence x in (UFilter BL) . (a "\/" b) by A5, A6, Th17; :: thesis: verum

end;

hence (UFilter BL) . (a "\/" b) = ((UFilter BL) . a) \/ ((UFilter BL) . b) by A1; :: thesis: verum